Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)

Imagina el mundo de las matemáticas como una ciudad inmensa y antigua. Durante siglos, la gente construyó casas de lógica por su cuenta, pero a menudo utilizaban diferentes planos, lo que dificultaba compartir herramientas o construir nuevos vecindarios juntos. Entonces llegó Mathlib, una gran biblioteca centralizada donde matemáticos de todo el mundo acordaron construir sus demostraciones utilizando el mismo lenguaje y las mismas reglas. Es como un traductor universal para las matemáticas, que convierte ideas complejas y aisladas en un paisaje urbano compartido y verificado, donde todos pueden ver exactamente cómo se construyó un puente y confiar en que no se derrumbará.

Ahora, imagina que la Ciencia de la Computación es la próxima gran ciudad que espera ser construida. Es el estudio de cómo le decimos a las máquinas que piensen, se muevan y resuelvan problemas. Pero, al igual que la antigua ciudad de las matemáticas, la ciencia de la computación ha sido a menudo una colección de talleres aislados. Este artículo presenta CSLib, un nuevo proyecto que pretende hacer por la ciencia de la computación lo que Mathlib hizo por las matemáticas: crear un hogar único y compartido para todas las reglas, lenguajes y modelos que utilizamos para describir el software. La gran pregunta aquí es simple pero enorme: ¿Podemos construir una "columna vertebral" de la ciencia de la computación que sea tan sólida y estandarizada que podamos verificar formalmente nuestro software y modelos, tal como se demuestra un teorema matemático? Si podemos lograrlo, significa que podríamos construir sistemas digitales con propiedades matemáticamente verificadas, en lugar de depender únicamente de las pruebas para encontrar errores.

El nuevo eje de la ciudad digital

Piensa en CSLib como el sistema nervioso central para una creciente ciudad digital. Así como una ciudad necesita una columna vertebral robusta para sostener sus rascacielos y puentes, la ciencia de la computación necesita una base sólida de reglas verificadas para soportar el complejo software que usamos todos los días. Este artículo presenta el plano de esa columna vertebral. No solo construye unas cuantas habitaciones al azar; establece los principios fundacionales, las reglas de operación y el marco semántico (que es solo una forma elegante de decir "el diccionario y la gramática") para cómo hablamos de los programas informáticos, algo con lo que todos en esta nueva biblioteca estarán de acuerdo.

Los autores están construyendo esta biblioteca sobre los hombros de gigantes, siguiendo específicamente los pasos de Mathlib. Están tomando la misma receta exitosa que funcionó para las matemáticas puras y aplicándola al mundo desordenado y práctico de la ciencia de la computación. El objetivo es crear un lugar donde las ideas sobre lenguajes de programación y modelos de software puedan ser almacenadas, comprobadas y reutilizadas por cualquier persona, en cualquier lugar.

Las herramientas del oficio

Para que esta biblioteca funcione, el artículo introduce algunas herramientas ingeniosas que actúan como el equipo de construcción para nuestra ciudad digital.

Primero, han construido interfaces semánticas reutilizables. Imagina que intentas explicar cómo se mueve un personaje de un videojuego. Podrías describir cada fotograma de animación, o podrías usar un conjunto estándar de reglas, como "si el jugador presiona 'A', el personaje salta". En CSLib, los autores han creado "libros de reglas" estándar para dos tipos específicos de movimiento: reducción (cómo un programa se simplifica paso a paso) y sistemas de transición etiquetados (cómo un programa pasa de un estado a otro, como un semáforo que cambia de rojo a verde). Estos no son solo descripciones aisladas; son interfaces reutilizables. Esto significa que si quieres demostrar algo sobre un nuevo lenguaje de programación, no tienes que reinventar la rueda. Simplemente puedes conectar tu nuevo lenguaje a estos libros de reglas existentes y confiables.

Segundo, el artículo destaca la automatización de pruebas. En los viejos tiempos, demostrar que un fragmento de software era correcto era como revisar manualmente cada uno de los ladrillos de una pared. Era lento y propenso al error humano. Los autores han contribuido con herramientas que actúan como un asistente robótico súper rápido. Esta automatización ayuda a verificar las demostraciones, asegurando que la lógica se mantenga sin que un humano tenga que observar cada línea de código. Es como tener un corrector ortográfico para la lógica que nunca se cansa.

Tercero, han establecido un soporte de CI/pruebas. En el mundo del software, "CI" significa Integración Continua, que es básicamente una red de seguridad. Cada vez que alguien añade una nueva pieza a la biblioteca, un sistema automatizado comprueba que no rompa nada más. El artículo señala que este sistema está diseñado para mantener la compatibilidad de la nueva biblioteca de ciencias de la computación con la antigua biblioteca de matemáticas (Mathlib). Es como asegurar que la nueva autopista digital se conecte perfectamente con los puentes matemáticos existentes, para que el tráfico pueda fluera fluidamente entre los dos mundos.

¿Qué hay realmente allí?

El artículo no solo habla de las herramientas; muestra que ya se están utilizando. Los autores han contribuido con los primeros desarrollos sustanciales de lenguajes y modelos dentro de este nuevo marco. Esto significa que no solo han construido el andamiaje; de hecho, han comenzado a construir los primeros edificios. Han tomado conceptos del mundo real de los lenguajes de programación y los modelos y los han formalizado con éxito utilizando su nuevo sistema.

Sin embargo, es importante entender el alcance de lo que se ha logrado. El artículo presenta estos avances como principios fundacionales y desarrollos iniciales. Sugiere que este enfoque funciona y proporciona un marco sólido para el futuro, pero no afirma haber resuelto todos los problemas de la ciencia de la computación. El trabajo se describe como una biblioteca de "crecimiento rápido", lo que implica que es un proyecto vivo y en constante evolución que aún está en construcción. Los autores demuestran que la base es sólida y que las primeras habitaciones están amuebladas, pero la ciudad está lejos de estar terminada.

Por qué es importante

Entonces, ¿por qué debería importarle a un adolescente curioso una biblioteca de ciencias de la computación formalizadas? Porque esta es la diferencia entre construir una casa de cartón y construir una de acero. Cuando escribimos software hoy en día, a menudo lo probamos para ver si se rompe. Si no se rompe, asumimos que es seguro. Pero con CSLib, el objetivo es crear una biblioteca compartida y verificada donde las reglas y los modelos del software puedan ser rigurosamente comprobados. Al centralizar estas ideas y proporcionar las herramientas para automatizar el proceso de verificación, los autores están allanando el camino para un desarrollo de software donde las propiedades críticas puedan ser verificadas matemáticamente.

El artículo sostiene que, al centralizar estas ideas y proporcionar las herramientas para automatizar el proceso de verificación, podemos construir un futuro donde la "columna vertebral" de nuestro mundo digital sea inquebrantable. Es una visión lúdica y ambiciosa donde el caos de la programación es domado por el orden de las matemáticas, creando un paisaje digital que no es solo funcional, sino fundamentalmente confiable.