Xavier Leroy, investigador francés del Inria y creador del lenguaje de programación OCaml, protagoniza una entrevista en profundidad en el podcast The Peterman Pod, conducido por Ryan Peterman. El episodio, de una hora y veinticuatro minutos, recorre la trayectoria de Leroy en compiladores, lenguajes funcionales y verificación formal de software, y sirve como recurso divulgativo para quienes se acercan por primera vez a estas disciplinas.
A lo largo de la conversación se desgranan las claves que diferencian a OCaml de otros lenguajes (Rust, JavaScript, C), el funcionamiento de la inferencia de tipos y la razón por la que la gestión manual de memoria puede ofrecer mayor rendimiento. Leroy dedica un bloque amplio a explicar qué es la verificación formal y cómo se aplica en proyectos como el compilador certificado CompCert o el micronúcleo seL4. También aborda la complejidad de incorporar soporte multinúcleo a OCaml, la interoperabilidad entre lenguajes y los riesgos de un código generado por modelos de lenguaje casi correcto pero no del todo fiable.
El episodio incluye además reflexiones sobre el impacto de los grandes modelos de lenguaje en el diseño de lenguajes de programación, la tensión entre investigación académica y trabajo industrial, los problemas abiertos más interesantes del campo y recomendaciones de libros como Programming Pearls y How to Design Programs. La pieza incorpora patrocinio de WorkOS y enlaces al proyecto de teclado ergonómico Compose del anfitrión.