Las proposiciones son tipos, las demostraciones son programas

Traducción automática del original en inglés, todavía sin revisar. Leer el original.

En la década de 1930, Haskell Curry notó algo raro. Estaba trabajando en lógica combinatoria, un sistema para manipular funciones abstractas, y se dio cuenta de que las reglas que gobernaban sus combinadores se veían idénticas a las reglas de un sistema lógico llamado lógica proposicional intuicionista. Era como si hubiera encontrado dos mapas distintos del mismo territorio.

Tres décadas después, William Howard encontró lo mismo en un contexto más rico. Mostró que el cálculo lambda simplemente tipado, la base de la programación funcional, se corresponde exactamente con la deducción natural, un sistema estándar de demostración lógica. Cada tipo corresponde a una proposición. Cada programa corresponde a una demostración. Cada función corresponde a una implicación.

Esta es la correspondencia de Curry-Howard: una identidad estructural entre demostraciones y programas.

#¿Qué es la matemática?

Desde afuera, la matemática parece cálculo: multiplicá estos números, despejá x, calculá una integral. Pero el cálculo es a la matemática lo que tipear es a la programación: una habilidad básica, no la cosa en sí.

La matemática es el estudio de lo que tiene que ser verdadero dado un conjunto de supuestos iniciales. Elegís tus axiomas, los enunciados que aceptás sin demostración (como “cero es un número natural” o “todo número natural tiene un sucesor”). Después aplicás reglas de inferencia para derivar enunciados nuevos. Si seguís las reglas al pie de la letra, tus conclusiones están garantizadas como verdaderas dentro de ese sistema. No probablemente verdaderas. No verdaderas según un experimento. Lógica y necesariamente verdaderas.

Una demostración es lo que hace que esto funcione. Una demostración es una cadena de pasos, cada uno justificado por una regla, que arranca en los axiomas y termina en lo que querés mostrar. Pensalo como un juego de mesa. No discutís si una jugada de ajedrez es legal. O la pieza puede ir ahí o no puede. Una demostración es un registro completo de jugadas legales desde la posición inicial hasta la afirmación final.

Esto tiene una consecuencia notable: las demostraciones son mecánicas. No necesitás intuición ni genio para verificar una demostración. Solo tenés que comprobar que cada paso sale de las reglas. Una máquina podría hacerlo. De hecho, eso es exactamente lo que hacen los demostradores de teoremas interactivos (interactive theorem provers). Sistemas como Lean, Coq y Agda te dejan escribir demostraciones matemáticas como código. Si el código compila, la demostración es válida. Si no compila, te equivocaste, y el sistema te dice dónde.

Estas herramientas no son juguetes. La biblioteca matemática de Lean contiene un cuerpo muy grande de matemática verificada formalmente. Coq se usó para construir CompCert, un compilador de C verificado que se usa en la industria aeroespacial. El microkernel seL4, verificado en Isabelle/HOL, corre en helicópteros militares. HACL*, una biblioteca criptográfica verificada, viene incluida en Firefox y en Linux.

• Las proposiciones son enunciados que son verdaderos o falsos: “1 + 1 = 2”, “todo número par mayor que 2 es la suma de dos primos”
• Las demostraciones son derivaciones paso a paso de que una proposición es verdadera
• Los axiomas son las proposiciones iniciales que aceptás sin demostración
• Las reglas de inferencia te dicen cómo derivar verdades nuevas a partir de las que ya tenés (por ejemplo: si sabés A y sabés “A implica B”, podés concluir B)
• Una demostración es válida cuando cada paso sale de las reglas, y verificar eso es mecánico.

La matemática es un juego de seguir reglas lo bastante preciso como para que una máquina lo verifique.

#¿Qué es un tipo, en serio?

La mayoría de los programadores conoce los tipos primero como etiquetas: int, string, bool, List<User>. Eso es útil, pero esconde la parte interesante. Un tipo es una afirmación sobre qué valores están permitidos y qué operaciones tienen sentido sobre ellos.

Cuando escribís x: int, estás haciendo una afirmación: “x siempre va a ser un entero”. El compilador te hace cumplirla. Un tipo es una restricción que el compilador verifica antes de que tu código corra.

Los tipos simples expresan restricciones simples: int significa “esto es un entero”. Los tipos más complejos expresan restricciones más complejas:

• List<String> significa “una lista donde cada elemento es un string”
• (String) -> Int significa “una función que toma un string y devuelve un entero”
• En Rust, &'a str significa “una referencia a un string que está garantizado que es válida durante el lifetime 'a”

El compilador verifica todo esto antes de que el programa corra. Si las restricciones no se cumplen, el código no compila.

Cada vez que el compilador acepta tu código, demostró algo. Cuando Rust acepta un programa, demostró que no hay punteros colgantes (dangling pointers), ni data races, ni bugs de use-after-free. Son teoremas reales sobre el comportamiento de tu programa, verificados en tiempo de compilación. El compilador de Rust es un demostrador de teoremas especializado que no se llama a sí mismo así.

Pero no todo sistema de tipos puede expresar cualquier afirmación. Los tipos de Rust pueden hablar de ownership de memoria y de lifetimes, pero no pueden enunciar “todo número par mayor que 2 es la suma de dos primos”. Los tipos de TypeScript pueden hablar de la forma de los objetos, pero no de la corrección de un ordenamiento. Estos lenguajes exponen fragmentos de una idea más profunda: los tipos son afirmaciones verificadas por una máquina. Los asistentes de demostración (proof assistants) como Lean llevan esa idea hasta el final, así que las afirmaciones pueden hablar de la matemática misma, no solo de strings, listas o lifetimes.

Detrás de esto hay un modelo formal de cómputo, igual que la lógica está detrás de la demostración matemática. El que más importa acá es el cálculo lambda: variables, funciones y aplicación de funciones. Cuando escribís código común, ya estás trabajando en descendientes de esa tradición. Curry-Howard importa porque conecta ese mundo de programas tipados con el mundo de las demostraciones formales.

#Dos mundos formales

Entonces tenemos dos mundos formales:

	Matemática	Cómputo
Objetos	Proposiciones	Tipos
Evidencia	Demostraciones	Programas (valores)
Reglas	Reglas de inferencia	Reglas de tipado
Verificación	Verificación de demostraciones	Chequeo de tipos
Fundamento	Lógica formal	Cálculo lambda

Los dos son juegos de seguir reglas. Los dos tienen fundamentos precisos de la década de 1930. Los dos se pueden verificar mecánicamente.

Curry-Howard dice que son el mismo juego.

#La correspondencia

La tabla de arriba es la vista general. Curry-Howard hace que cada fila sea precisa y mecánica:

Lógica	Programación
Un enunciado que puede ser verdadero o falso	Un tipo
Una demostración de que un enunciado es verdadero	Un valor de ese tipo
“Si A entonces B”	Una función del tipo A al tipo B
“A y B”	Un par (A, B)
“A o B”	Una unión etiquetada / tipo suma
“Para todo x, P(x) es verdadero”	Una función genérica que anda para cualquier x
“Falso” (una contradicción)	Un tipo sin valores

Esto va más allá de compartir notación. Las reglas que hacen válidas a las demostraciones y las reglas que hacen que los programas pasen el chequeo de tipos son las mismas reglas, descubiertas de forma independiente en dos campos distintos.

#Los enunciados son tipos

El enunciado matemático “1 + 1 = 2” corresponde a un tipo específico. Si podés crear un valor de ese tipo siguiendo las reglas, el enunciado es verdadero. Si ningún valor así puede existir, el enunciado es falso.

En un asistente de demostración como Lean, escribirías el tipo directamente como 1 + 1 = 2. En el demostrador chiquito que vamos a construir en el próximo artículo, se va a ver más explícito y más mecánico. La notación cambia. La idea es la misma: la proposición es el tipo.

#Las demostraciones son valores

En programación, demostrás que un tipo “existe” construyendo un valor de ese tipo. 42 demuestra que el tipo Int está habitado. [1, 2, 3] demuestra que List<Int> está habitado. Del mismo modo, si podés construir un valor de un tipo-proposición usando solo reglas legítimas, demostraste la proposición.

Por eso la correspondencia es exacta y no aproximada. Una demostración no es un relato sobre por qué algo es verdadero. Es un objeto concreto, un término que el type checker puede inspeccionar, descomponer y verificar mecánicamente.

#Las funciones son implicaciones

Una función del tipo A al tipo B dice: “dame evidencia de A y te produzco evidencia de B”. Eso es exactamente lo que significa “si A entonces B” en lógica. El cuerpo de la función es la derivación.

Si tenés una función f: A -> B y tenés un valor a: A, entonces f(a) te da un valor de tipo B. En lógica: si sabés “A implica B” y sabés “A”, entonces sabés “B”. Eso es modus ponens, una de las reglas de inferencia más viejas, y es literalmente aplicación de funciones.

#Los pares son conjunciones

Un par (a, b) donde a: A y b: B es evidencia de que valen tanto A como B. Para construirlo, necesitás evidencia de cada uno. Para usarlo, podés proyectar cualquiera de los dos componentes. Esto coincide exactamente con cómo funciona la conjunción (el “y” lógico): para demostrar “A y B”, demostrá los dos; dado “A y B”, podés concluir cualquiera de los dos.

#Los tipos suma son disyunciones

Una unión etiquetada (como el enum de Rust o el Either de Haskell) que contiene o un valor de tipo A o un valor de tipo B es evidencia de que vale al menos uno de A o B. Para construirla, necesitás evidencia de uno. Para usarla, tenés que manejar los dos casos. Esto es el “o” lógico: para demostrar “A o B”, demostrá uno de los dos; dado “A o B”, razoná por casos.

#Las funciones genéricas son enunciados universales

“Para todo n, P(n) es verdadero” simplemente significa: escribí una función que tome cualquier n y devuelva un valor de tipo P(n). Si la función compila para todas las entradas, demostraste el enunciado universal. No hace falta ninguna maquinaria especial para cuantificadores. Es simplemente programación genérica, lo mismo que hacés cuando escribís una función que anda sobre cualquier lista sin importar el tipo de sus elementos.

#Falso es un tipo vacío

Una proposición que nunca se puede demostrar corresponde a un tipo sin valores. Podés escribir el tipo (podés enunciar la proposición), pero nunca podés construir un valor de ese tipo (nunca podés demostrarla). “No P” entonces significa “una función de P al tipo vacío”: si suponer P te deja producir un valor de un tipo deshabitado, algo salió mal, y P tiene que ser falsa. Esto es demostración por contradicción codificada como una función.

#Por qué importa

#Los compiladores ya están demostrando teoremas

Esto significa que el chequeo de tipos, lo que los compiladores ya hacen cuando rechazan "hello" + 3, es una forma de verificación de demostraciones. Cuando Rust acepta tu código, demostró seguridad de memoria. Cuando Haskell chequea los tipos de código con GADTs, demostró que tus invariantes se cumplen. Cuando un smart contract verificado pasa su type checker, propiedades como “esta función nunca transfiere más tokens que el saldo” quedan establecidas en tiempo de compilación.

El mecanismo es el mismo en todos estos sistemas. La diferencia es el alcance. Rust demuestra un conjunto fijo de propiedades de memoria. Lean demuestra lo que le pidas.

#Los asistentes de demostración son lenguajes de programación

Lean, Coq y Agda no están separados del mundo de la programación. Son lenguajes de programación donde el sistema de tipos es lo bastante expresivo como para enunciar proposiciones matemáticas arbitrarias. “Demostrá este teorema” significa “construí un valor de este tipo”. Las herramientas, las tácticas (tactics) y la automatización apuntan a hacer más fácil esa construcción, pero en el fondo es la misma actividad que escribir un programa que pasa el chequeo de tipos.

#La frontera entre programación y matemática es artificial

La distinción entre programar y demostrar es artificial. Una función de ordenamiento que devuelve un valor de tipo “una lista ordenada más una demostración de que es una permutación de la entrada” está haciendo las dos cosas a la vez: calcular y demostrar. Los lenguajes con tipos dependientes como Lean, Agda e Idris te dejan escribir programas que llevan consigo sus demostraciones de corrección.

#Alcance y límites

La correspondencia es exacta en los sistemas formales adecuados (el cálculo lambda simplemente tipado corresponde a la lógica proposicional intuicionista, System F corresponde a la lógica de segundo orden, y así). Pero los lenguajes de programación reales son desprolijos. La mayoría tiene características que rompen la correspondencia:

• Recursión general. Si un lenguaje te deja escribir loops infinitos, podés “demostrar” cualquier cosa: una función que no termina de tipo A -> B técnicamente tiene el tipo correcto pero no produce ninguna evidencia. Los asistentes de demostración exigen terminación para que la lógica siga siendo consistente (sound).
• Excepciones y efectos. Tirar una excepción desde adentro de una función de tipo A -> B significa que nunca llegás a producir un B. Los efectos secundarios debilitan de manera parecida la interpretación lógica.
• Vías de escape inseguras. El unsafe de Rust, el unsafePerformIO de Haskell y el any de TypeScript rompen la correspondencia porque te dejan saltear el type checker.

Por eso los asistentes de demostración son estrictos: nada de recursión general sin demostraciones de terminación, nada de efectos sin control, nada de vías de escape. Las restricciones que hacen que sea más difícil programar en ellos son exactamente las restricciones que mantienen consistente la lógica.

Los lenguajes de programación de todos los días exponen fragmentos de Curry-Howard. Los asistentes de demostración son lo que obtenés cuando la llevás hasta el final.

#Cómo seguir

El próximo artículo construye desde cero un demostrador de teoremas chiquito en Python. Vas a ver la arquitectura exacta: términos, tipos, un verificador y una frontera de confianza que podés señalar con un dedo. Después, el artículo de Julia muestra las mismas ideas metidas dentro del sistema de tipos de un lenguaje anfitrión, donde el propio compilador se vuelve el verificador de demostraciones.

#Lecturas recomendadas

• La guía de Fede sobre sistemas de tipos. Si querés más contexto sobre cómo funcionan en la práctica los sistemas de tipos, de los generics a los tipos dependientes, antes de meterte con las demostraciones.
• “Propositions as Types”, de Philip Wadler. El mejor panorama de la correspondencia, su historia y por qué sigue apareciendo. Disponible gratis en internet, y también como charla de conferencia (Strange Loop).
• “Types and Programming Languages”, de Benjamin Pierce. El libro de texto estándar. Los capítulos 9 a 11 cubren el cálculo lambda simplemente tipado; el capítulo 30 cubre la correspondencia.
• “The Little Typer”, de Friedman y Christiansen. Una introducción amable y socrática a los tipos dependientes, donde Curry-Howard se vuelve el principio central de diseño.
• “Software Foundations” (gratis en internet). Una introducción interactiva, basada en demostraciones, usando Coq.