Escalando el monte Everest de la programación informática

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.

Aleks Nanevski, investigador del Instituto IMDEA Software, descubrió su pasión por las matemáticas a los 10 años cuando un profesor de su colegio en Macedonia vio en él aptitudes y empezó a darle clases extraescolares. Desde entonces, comenzó a participar en competiciones regionales y a la edad de 13 ya estaba en el podio de las competiciones nacionales.

Aquel niño que despuntaba en el arte de las matemáticas pidió a sus padres un ordenador. Durante un viaje familiar a Francia, por fin sus padres pudieron comprarle uno, el que se podían permitir, y Aleks empezó a adentrarse en el mundo de la programación. Por desgracia, o quizá por suerte, el manual de instrucciones de aquella máquina estaba en francés y él no conocía el idioma. Durante un tiempo tampoco pudo conectar el ordenador a su televisor, debido a las diferentes normas de televisión, pero el manual mostraba programas de ejemplo en el lenguaje de programación BASIC junto con el resultado de su ejecución. Eso le bastó para aprender a programar mentalmente, sin tener que escribir nada en un ordenador

Su carrera como investigador empieza con su doctorado en la Universidad Carnegie Mellon, pasando por la Universidad de Harvard con un contrato posdoctoral para más tarde adentrarse en el mundo de la empresa en Microsoft Research en Cambridge y acabar en el Instituto IMDEA Software, lugar donde consiguió una beca ERC por valor de dos millones de euros por el proyecto “MATHADOR: Type and Proof Structures for Concurrent Software Verification”. 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.

Un programa informático, por ejemplo, de un coche eléctrico tiene millones de líneas de código y puede funcionar en el momento de su lanzamiento, pero eso no significa que no pueda tener errores. Encontrar los errores puede ser como buscar una aguja en un pajar, ya que implica tiempo y recursos. Si, además, el error surge de la interacción defectuosa entre componentes que funcionan simultáneamente, como podría ser la conexión con el GPS, los sensores de seguridad o una aplicación de música, las dificultades se multiplican. En principio, se puede pensar en buscar los errores, pero en la práctica esto requiere una cantidad de trabajo inviable. Para abordar realmente el problema, es necesario un enfoque radical.

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.

Coraje, valentía, paciencia y fe son algunas de las características que definen a un investigador que eligió el camino largo y difícil: «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ço 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.

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».

«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])»