Sistema · diseño, no está en ninguna versión
LSPE
Cada compilación es un conjunto de juicios sobre tu programa. LSPE obliga al compilador a responder por ellos: busca la fuente de cada juicio, te hace una pregunta registrada cuando no la encuentra y escribe el intercambio en el binario. No promete que tu programa sea correcto. Promete que ninguna excepción pasa en silencio.
Un diseño, no algo que se descarga
A 2026-10-18, LSPE es un diseño. Ninguna versión lo incluye, no hay nada que instalar y esta página
no pone fecha a su llegada. El diseño está escrito en el repositorio como docs/262
— en chino, como los demás documentos de diseño numerados: este proyecto guarda sus planes
ahí, no en un gestor público de incidencias.
Lo que sigue es para qué sirve el diseño y qué se niega a afirmar. No es el anuncio de una función que puedas activar.
Un diseño no es una promesa. Ya se sabe que dos cosas son imposibles, y el diseño las escribe en lugar de rodearlas: ningún compilador puede demostrar que un programa está libre de defectos, y ninguno puede resolver todas las preguntas que no sabe responder. Todo lo de abajo está moldeado por esos dos hechos.
Un recibo por cada decisión
Hoy un compilador te da un solo bit: el programa se acepta o se rechaza. Las razones se quedan dentro del compilador, y las suposiciones que hizo para llegar a «aceptado» no están escritas en ningún sitio que puedas revisar.
LSPE añade un registro. Cada vez que el compilador deja pasar algo que no pudo demostrar, el binario anota qué decisión era, en qué evidencia se apoyaba y — cuando una persona respondió a una pregunta — quién respondió. El binario lleva un hash de ese registro; la derivación queda al lado, fuera del binario, así que el binario no crece con ella.
Eso no es «sin defectos». Si un programa está libre de defectos no lo puede decidir un compilador; si cada excepción quedó escrita, sí. Lo primero es indecidible. Lo segundo es una propiedad del proceso, y puede comprobarla fuera de línea, a posteriori, alguien que no confíe en el compilador.
Las cuatro partes
LSPE son cuatro cosas que trabajan sobre un mismo espacio: los puntos de una unidad donde se tomó una decisión, las obligaciones que esos puntos cargan, la evidencia a su favor y el registro de qué pasó con cada uno. No es un quinto comprobador: los comprobadores se quedan donde están.
El que interroga
El compilador deja de ser solo un juez. Antes de aceptar una decisión, busca su fuente, intenta construir un contraejemplo y la contrasta con la segunda implementación. Si fallan las tres, tiene un agujero — y lo dice de sí mismo, no de que tu código esté mal.
Las preguntas
Un agujero se convierte en una pregunta con opciones, un valor por defecto y la consecuencia de cada respuesta. Tu respuesta queda registrada. Aplazar sin registrar es, en sí, un error de compilación, así que «sé que esto es sospechoso pero no sé explicar por qué» deja de ser conocimiento que solo vive en la cabeza de alguien.
La policía (LSPC)
Antes de la compilación te pasa la cuenta: qué riesgos residuales vas a aceptar, una línea por familia, con lo que ocurre si esa familia no se cumple. Por defecto no bloquea. Arreglas lo que quieras y dejas el resto, y lo que dejas es lo que queda registrado.
El libro mayor
Todo lo que deciden los demás componentes de seguridad — la escalera de reclamación, los niveles de seguridad de memoria, los dominios de capacidad, la propiedad — llega a un mismo libro mayor. Ninguno de esos componentes se sustituye ni se renombra; el libro es donde sus veredictos se pueden leer juntos y contrastar.
La carga de la prueba cambia de dirección
El compilador habitual está fuera del programa y anuncia un resultado. LSPE está dentro de la transacción: nombra su fuente, pone precio a lo que supone y te entrega un recibo. Cuando no puede demostrar algo, no puede decir «tu código está mal»; tiene que decir «mi demostración tiene un agujero aquí». Lo primero es una afirmación sobre ti, lo segundo sobre el compilador, y los dos se mantienen separados a propósito.
Esa separación tiene un costo, y el diseño lo paga: el que interroga guarda un registro de cada sustitución de tipos y vuelve a demostrar sus obligaciones después de cada una. El propio historial de Rust incluye un defecto de solidez exactamente de esa forma — una comprobación que se cumplía antes de una sustitución y no se volvió a ejecutar después. Un compilador que solo pregunta «¿hay fuente?» no lo detecta: la fuente existía, y había caducado.
Un dependiente no es una autoridad. La semántica pertenece al estándar y a cada componente. LSPE registra decisiones y les pone precio; no decide qué es verdad.
Lo que no hace
No encuentra más errores de memoria
Encuentra excepciones sin fuente y evidencia caducada. Un programa sin esas excepciones puede seguir estando mal.
No hace más seguro un programa
Hace imposible aceptar un riesgo residual en silencio. Son dos números distintos, y el diseño los mantiene separados en vez de cambiar uno por otro.
No sustituye a los comprobadores
La escalera de reclamación, los niveles de seguridad de memoria, los dominios de capacidad y la propiedad conservan sus nombres, sus dueños y sus criterios. LSPE lee sus veredictos.
No es una forma de comprobar menos
Cerrar la auditoría es una elección registrada que firmas, no un interruptor que quita comprobaciones. Las comprobaciones siguen corriendo igual; lo que cambia es si el resultado queda escrito.
La escalera de reclamación se describe en su propia página, y la autoridad
de cada obligación es el estándar. El documento de diseño es
docs/262 en el repositorio.