La pregunta que lo origina

Hay una distancia incómoda entre la lógica que se estudia y la lógica que se usa. En los textos, la lógica es un sistema de símbolos que se manipulan con la mano, sobre papel, siguiendo reglas que uno mismo vigila. En el software, la lógica es implícita: está escondida en los if, en los invariantes que nadie anotó, en los tipos que el compilador infiere sin que el programador lo sepa bien. Esa distancia entre el razonamiento explícito y el código que corre es el problema que ST intenta cerrar.

ST —Symbolic Theory Language— es un lenguaje ejecutable para lógica formal. No una biblioteca. No un verificador externo que se invoca como herramienta de diagnóstico. Un lenguaje con su propio léxico, su parser, su AST tipado, su intérprete, y su suite de 6333 tests que exige que cada pieza funcione antes de declarar que el sistema existe.

Lógica como ciudadano de primera clase

Lo que hace diferente a ST no es la variedad de perfiles lógicos que soporta, aunque esa variedad es real y técnicamente costosa de sostener. Lo que lo hace diferente es la decisión de diseño que subyace a todo: la lógica no es un añadido que se pega encima del lenguaje. Es el lenguaje mismo.

Cuando escribes en ST, no estás llamando a una función que evalúa una fórmula. Estás declarando una teoría, derivando conclusiones, verificando tautologías, construyendo contramodelos. El flujo de control —if, for, while, fn— existe al servicio de ese razonamiento, no al revés. Eso invierte la jerarquía habitual: en la mayoría de los lenguajes de programación, la lógica sirve al flujo de datos; en ST, el flujo de control sirve a la lógica.

Esta inversión tiene consecuencias prácticas. Una condición en un if no es un booleano en tiempo de ejecución: es una consulta de satisfacibilidad. while satisfiable estado significa exactamente lo que dice. El lenguaje fuerza al programador a pensar en términos de mundos posibles, no solo de estados de máquina.

El SAT solver que nadie esperaba

Soportar lógica clásica proposicional es relativamente sencillo. Soportarla bien, con performance, a escala, dentro de un lenguaje interpretado, requiere decisiones que los proyectos académicos usualmente evitan.

ST incluye un SAT solver CDCL propio —Conflict-Driven Clause Learning— con VSIDS, clause learning y reinicios según la secuencia de Luby. El solver es incremental: reutiliza estado entre consultas en lugar de reiniciar desde cero cada vez. CDCL es el núcleo de los solvers industriales modernos —los que verifican hardware y compiladores. Haberlo implementado desde cero, con esta cobertura de tests, no es un adorno.

Además está MUS: Minimal Unsatisfiable Subsets. Cuando una fórmula es insatisfacible, saber que lo es no basta. Saber por qué —cuál es el subconjunto mínimo de premisas que genera la contradicción— es lo que permite diagnosticar y corregir. ST lo expone como operación nativa.

Teoría de tipos como infraestructura

El salto de lógica proposicional a teoría de tipos es conceptualmente enorme. La correspondencia Curry-Howard dice que los tipos son proposiciones y los programas son pruebas. Es una de las ideas más profundas de la ciencia de la computación del siglo XX, y también una de las más difíciles de implementar de manera que sea usable.

ST implementa Martin-Löf Type Theory —MLTT— con tipos dependientes, System F con polimorfismo paramétrico, Normalización por Evaluación para reducción eficiente, y refinement types sobre términos base. Eso no es un recorrido turístico por la teoría de tipos. Es una infraestructura que permite expresar propiedades que los sistemas de tipos convencionales no pueden capturar: que una función solo acepta listas no vacías, que el índice de un arreglo siempre está en rango, que dos valores satisfacen una relación específica.

ST no es solo un lenguaje de scripting. Es un sistema de argumentación. Y argumentar con precisión requiere poder expresar con precisión qué tipo de cosa es cada cosa.

El problema de los mundos posibles

La lógica modal es la lógica de la necesidad y la posibilidad. Suena abstracto hasta que aparece en contextos concretos: verificación de protocolos de concurrencia, razonamiento sobre conocimiento en sistemas multiagente, formalización de obligaciones en contratos.

ST soporta los sistemas modales estándar —K, T, B, S4, S5, KD45— más CTL para árboles de computación, LTL para trazas lineales, y μ-cálculo modal con puntos fijos mínimos y máximos. La mayoría de los bugs no son errores de aritmética: son errores de razonamiento sobre el tiempo, el orden, la concurrencia. Un sistema que puede verificar siempre eventualmente P o P hasta que Q tiene herramientas para ese problema.

La Text Layer: donde el lenguaje toca el mundo

Hay una característica de ST que no tiene equivalente en los sistemas de lógica que conozco: la Text Layer. Permite vincular pasajes de documentos reales —contratos, artículos, especificaciones— con formalizaciones lógicas y claims verificables.

let p = passage([[contrato.md#clausula-1]])
let f = formalize p as (P -> Q)
claim c1 = f
support c1 <- p
confidence c1 = 0.92

Esto es ambicioso de una manera particular. No es solo formalización de matemáticas: es un intento de dar a los documentos en lenguaje natural una estructura lógica ejecutable. La cláusula de un contrato como premisa de una derivación. Un argumento filosófico como teoría que se puede verificar. La idea de que el texto humano y la lógica formal no tienen que vivir en mundos separados.

La v2 de esta capa agrega invalidación propagada de claims y un bridge bidireccional con MDX, lo que sugiere que el objetivo no es académico sino práctico: razonamiento asistido por máquina sobre documentos reales.

Lo que enseña construir esto

Hay proyectos que enseñan tecnología y proyectos que enseñan a pensar. Construir un SAT solver CDCL obliga a entender la búsqueda con retroceso, el aprendizaje de cláusulas, la geometría del espacio de soluciones. Implementar MLTT obliga a entender la correspondencia entre prueba y programa en un nivel que ningún tutorial de tipos explica. Soportar 30 perfiles lógicos coherentes obliga a diseñar abstracciones que soporten variación sin colapsar en caos.

Los 6333 tests no son una métrica de vanidad. Son la única manera honesta de saber que un sistema con esta complejidad hace lo que dice. En conjunto son una especificación ejecutable del lenguaje.

ST plantea una pregunta que vale la pena sostener: ¿qué pasaría si el razonamiento formal fuera tan accesible como escribir un script? No como herramienta de especialistas, sino como modo natural de pensar en código. La respuesta está construyéndose, pero la pregunta es la correcta.