Todo programa bien tipado es una demostración. Todo tipo es una proposición. No es una metáfora: es un teorema matemático descubierto en los años 30 que explica por qué hacer los estados inválidos irrepresentables realmente funciona.
Agregar un nuevo tipo es facil en OOP, dificil en FP. Agregar una nueva operacion es facil en FP, dificil en OOP. Philip Wadler nombro esto el Expression Problem en 1998. Mostramos como se manifiesta en Rust y Scala, y anticipamos la resolucion.
Tu expresion match es semantica operacional. Tu funcion pura es semantica denotacional. El borrow checker de Rust es semantica axiomatica. Tres marcos formales, tres formas de asignar significado al codigo, y has estado usando los tres sin saberlo.
Cada enum que escribes es una gramatica formal. Cada sealed trait es un conjunto de reglas de produccion. Has estado haciendo metodos formales todo este tiempo; simplemente no sabias el nombre. Trazamos la conexion desde la jerarquia de Chomsky hasta tus tipos de dominio en Rust y Scala.
Al volver sobre el trait TaskRepository de la serie Todo CLI, me di cuenta de que no solo estaba dibujando una frontera arquitectónica. También estaba definiendo qué podía decirse en esa frontera, y eso se parece mucho más a una gramática de lo que pensé al principio.