Aleks Nanevski ha dedicado su vida a resolver uno de los mayores retos de la informática, emprendiendo un largo y arriesgado camino para revolucionar nuestra forma de concebir la programación en general, y la programación concurrente en particular.
Al investigador del Instituto IMDEA Software, Aleks Nanevski, le concedieron una beca ERC por MATHADOR: Type and Proof Structures for Concurrent Software Verification, en abril de 2017 por valor de dos millones de euros. El proyecto, financiado por el programa Horizonte Europa 2020, ha tenido una duración de 6 años y finalizó el pasado 31 de marzo. Su investigación, como indicó el European Research Council en el momento de la concesión de la beca, es de alto riesgo porque propone nuevos fundamentos para la verificación concurrente de software, pero también es muy beneficiosa, ya que la verificación de software concurrente es uno de los problemas abiertos más importantes de la investigación actual sobre lenguajes de programación y semántica.
La programación funcional y la teoría de tipos; centrados en el mundo académico, tienen sus raíces en la filosofía, la lógica y las matemáticas constructivas. Según Aleks: “puede que los programas funcionales no sean tan rápidos de ejecutar como los imperativos (los que utiliza la industria del software), pero son mucho más fáciles de escribir y de entender”. Un programa imperativo con cientos de líneas de código puede reducirse a menudo a unas pocas líneas en el lenguaje funcional. “Cuando programamos imperativamente, nos adaptamos a las máquinas, en cambio, cuando programamos funcionalmente, hacemos que las máquinas se adapten a nosotros” comenta Nanevski. La idea de la programación funcional es utilizar un lenguaje matemático tan minimalista, conciso y eficaz que facilite detectar los errores de programación, que permita no cometer errores desde el principio.
Aleks explica que su investigación está relacionada con “todo y nada al mismo tiempo. Es un problema fundacional, lo que implica que está muy idealizado. Toma sus retos de las prácticas y tecnologías existentes y elimina el desorden del mundo real, al tiempo que se esfuerza por destilar la cuestión básica fundamental. Esto hace que no tenga relación directa con nada, pero también lo relaciona con todo, porque esa cuestión central es lo que significa que los programas interactúen y se coordinen entre sí, y esta interacción surge en la Inteligencia Artificial, en el Internet de las Cosas y en todos los ámbitos intermedios. Debido a su universalidad, entender la cuestión matemáticamente abrirá posibilidades para las tecnologías del futuro que hoy ni siquiera podemos imaginar”.
“Empecé con la intuición de que la concurrencia debería ser abordada fructíferamente por la programación funcional y la teoría de tipos, porque las apliqué previamente a la programación no concurrente, lo que me permitió descubrir profundas conexiones con la llamada Lógica de Separación, una idea importante y bien conocida en informática. Sorprendentemente, hasta ahora esta intuición siempre se ha materializado, incluso cuando temporalmente parecía que no tenía ninguna posibilidad. Sin embargo, aún queda mucho camino por recorrer”, afirma Nanevski.
“Este proyecto ha recibido financiación del Consejo Europeo de Investigación (ERC) en el marco del programa de investigación e innovación Horizonte 2020 de la Unión Europea (Acuerdo de subvención nº [724464])”
