Tale area studia i metodi formali per una descrizione completa e non ambigua del significato dei programmi e dei linguaggi di programmazione. La loro applicazione alla pratica programmativa è rivolta ad aumentare l'affidabilità del software, mettendo a disposizione strumenti per l'analisi, la verifica, la trasformazione di programmi, e per la progettazione e valutazione di linguaggi di programmazione. I metodi di semantica formale si distinguono in funzione della prospettiva adottata. Si parla di semantica denotazionale se il significato di un programma viene visto come una funzione tra i dati di ingresso e quelli di uscita; si parla di semantica assiomatica se è caratterizzata per mezzo delle proprietà che il programma soddisfa, relativamente ad un certo linguaggio formale di descrizione; infine si parla di semantica operazionale quando il significato di un programma è identificato con il comportamento di un esecutore ideale, formalmente definito. In tutti i casi comunque, si ha una rappresentazione di un linguaggio di programmazione in termini di entità matematiche, la cui natura consente l'utilizzo di tecniche algebriche e logico-matematiche. Sotto la spinta di problemi sollevati da tale studio si è avuta una fioritura vastissima di teorie e metodi matematici ormai altamente specializzati, spesso in relazione alle classi di linguaggi più innovativi (e.g. funzionali, logici, e concorrenti).