Hace poco falleció Robin Milner, uno de mis modelos del investigador en informática. Estudió matemática y contribuyó a formar una de las mejores escuelas de computación del mundo en Edimburgo.
Mi primer contacto con su trabajo fue desentrañar el lenguaje Standard ML a partir de su definición matemática. ML era el metalenguaje para manipular fórmulas en un sistema lógico sobre funciones computacionales: Logic for Computable Functions (LCF). Milner diseñó ML como un lenguaje funcional en el que toda frase escrita por el programador tuviera el tipo más general posible sin que hubiera problemas de ejecución provocados por tipos, ¡sin que el programador tuviese que declarar los tipos de las variables!
Milner procedió a definir la semántica de un ML estandarizado. Esta definición y su comentario, son modelos de claridad y precisión para los estándares en informática: constituyen la base para la implementación del lenguaje y los sistemas para razonar acerca de sus programas. ML y su disciplina de tipos ha influido el diseño de muchos lenguajes de programación para el cómputo confiable.
Fue el primero en enunciar los conceptos de simulación de un tipo de datos por otro y de un modelo completamente abstracto de un lenguaje de programación.
Formuló un cálculo para especificar y diseñar sistemas con concurrencia y comunicación, con un método de razonamiento formal para demostrar sus propiedades. CCS, el Cálculo Pi y sus sucesores han abierto la senda para desarrollar protocolos de comunicación y sistemas concurrentes cuyas propiedades pueden garantizarse por diseño.
Milner se preguntaba “¿Es la computación una ciencia experimental?” Al aplicar modelos y teorías, podemos validarlos y mejorarlos. La formalización, al ser aplicada, también es experimentación.
Artículo publicado en el periódico El Financiero
