Semântica formal é a área de estudo de ciência da computação que se preocupa em especificar o significado (ou comportamento) de programas de computador e partes de hardware.
A semântica é complementar à sintaxe de programas de computador, que se preocupa em descrever as estruturas de uma linguagem de programação.
A necessidade de uma semântica formal (matemática) para linguagens de programação, justifica-se, pois:
Pode revelar ambiguidades na definição da linguagem (o que uma descrição informal não permitiria revelar);
É uma base para implementação (síntese), análise e verificação formal.