La semantica operazionale è un approccio fondamentale nello studio del significato dei linguaggi di programmazione, che ha avuto origine negli anni '60. Fu introdotta da Robert W. Floyd e successivamente formalizzata da Tony Hoare e Gordon Plotkin come una risposta alla necessità di descrivere in modo preciso il comportamento di programmi eseguiti da macchine astratte.
Il primo impulso significativo si ebbe con i lavori di Floyd, che propose l’idea di associare il significato dei programmi alle loro azioni osservabili durante l'esecuzione. Questo approccio venne ulteriormente raffinato da Hoare, con la sua logica assiomatica per il ragionamento sui programmi, nota come logica di Hoare.
La svolta cruciale arrivò nel 1981, quando Gordon Plotkin pubblicò il celebre articolo "A Structural Approach to Operational Semantics", in cui introdusse una metodologia sistematica e matematica per definire la semantica dei linguaggi: la Semantica Operazionale Strutturale (SOS). Questo schema utilizzava regole di inferenza per descrivere come le istruzioni di un linguaggio evolvono passo dopo passo.
Negli anni successivi, la semantica operazionale è diventata uno standard nella definizione formale dei linguaggi, utile sia in ambito teorico che pratico. È stata adottata in numerosi strumenti di verifica, compilatori e ambienti di sviluppo formale, contribuendo a garantire la correttezza dei software.
Oggi, la semantica operazionale continua a essere una pietra miliare dell’informatica teorica e della progettazione dei linguaggi di programmazione, grazie alla sua capacità di fornire descrizioni precise, modulari e facilmente comprensibili del comportamento dinamico dei programmi.