Un artículo divulgativo del ingeniero Ralf Jung, exresponsable del equipo de Rust en Google, acerca la investigación en lenguajes de programación (PL) al desarrollador medio a partir de un concepto muy concreto: la seguridad de memoria. Jung defiende que la seguridad de memoria es, ante todo, un asunto de diseño de lenguajes, y que la ciencia de los PL —a menudo vista como abstrusa— ofrece herramientas prácticas para entender, especificar y verificar el comportamiento del código.
El texto gira en torno a la semántica formal, es decir, a cómo definir con precisión matemática lo que significa un programa. Para ello introduce un lenguaje «de juguete» con aritmética, variables inmutables (let) y mutables (var), y lo analiza desde los tres enfoques clásicos. La semántica operacional describe paso a paso cómo se ejecuta el código en una máquina abstracta; es la base de especificaciones como ECMAScript y equivale, en la práctica, a escribir un intérprete. La semántica denotacional traduce cada programa a una función matemática que mapea estados de entrada en estados de salida, lo que permite demostrar equivalencias entre fragmentos de código y sustenta lenguajes funcionales puros como Haskell. La semántica axiomática, expresada mediante triples de Hoare ({P} C {Q}), define el significado de un programa por su efecto sobre proposiciones lógicas: si la precondición P se cumple antes de ejecutar C, entonces la postcondición Q se cumplirá después. Es el fundamento de la verificación formal y de herramientas como Coq o Dafny.
Jung subraya que las tres visiones son complementarias y útiles en distintos contextos, desde la definición de estándares hasta la verificación de software crítico como el de la ESA.