Tu primera prueba

diez minutos · tres pasos · nada que tengas que dar por sentado

Este es el camino para principiantes. No necesitas ser programador, no necesitas una cuenta, y no necesitas decirnos que existes. Al final de esto, tu propia computadora — no la nuestra, y no nuestra palabra — habrá comprobado las matemáticas detrás de una regla real de la biblioteca.

Si ya conoces bien un probador, el recorrido completo va más allá: construir el frontend y comprobar cada fila de su tabla de verdad. Esta página se detiene en la prueba, que es la parte que más importa y la que no necesita nada instalado.

Lo que estás a punto de comprobar

La regla se llama brief-fill policy. Decide cuándo un asistente puede responder en nombre de su propietario en lugar de preguntarle. Se hacen cuatro afirmaciones sobre ella, y las cuatro están a punto de ponerse a prueba en tu máquina:

• nunca rellena una respuesta sin una regla que la autorice;
• si el almacén de reglas falta, no pasa nada;
• nunca inventa nada;
• nunca te pregunta algo que una regla ya responde.

Estas no son promesas en una entrada de blog. Son teoremas, y un probador está a punto de intentar romperlos.

Paso 1 — consigue el probador

Es gratis y no es nuestro — viene de la comunidad Ada, no de nosotros. Ese es el punto: lo que comprueba nuestro trabajo no debería ser algo que te hayamos entregado nosotros.

Paso 2 — consigue la regla

Puedes ignorar la suma de comprobación en un primer intento — la prueba del paso 3 no depende de ella. Está ahí para cuando quieras confirmar que el archivo que recibiste es el que publicamos, y que es el mismo que nombra el catálogo.

Paso 3 — pide a tu computadora que lo compruebe

Abre una terminal en la carpeta descomprimida y ejecuta dos líneas:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2

Espera. Cuando termine, busca estas dos palabras:

0 unproved

Eso es todo. Ese es todo el ejercicio. No hace falta instalar nada más, y este paso funciona en una máquina sencilla sin nada más instalado — el probador que descargaste lleva todo lo que la prueba necesita.

Lo que acaba de pasar

Tu computadora tomó las cuatro afirmaciones anteriores, intentó encontrar un caso en el que alguna fallara, y no pudo — porque no existe. No es «lo probamos y parecía funcionar». No es «el mantenedor lo dice». Una máquina a la que no se puede convencer con palabras salió a buscar un contraejemplo y volvió con las manos vacías.

No confiaste en que te lo dijéramos nosotros. Lo viste ocurrir en hardware que es tuyo.

Opcional — rómpela a propósito

Esta es la parte que vale la pena hacer si tienes cinco minutos más, porque una comprobación que solo dice que sí siempre no vale gran cosa.

Abre brief_fill_policy_pkg.ads en cualquier editor de texto y cambia la regla para que un almacén ausente deje pasar una respuesta de todos modos. Ejecuta el mismo comando otra vez. Se negará — y nombrará el teorema exacto que acabas de romper.

Esa negativa es todo el modelo de seguridad. Ghillie no instala nada que no pase esto, así que lo que acabas de hacer a mano es lo que él hace en tu nombre cada vez.

Lo que esto no demuestra

Preferimos decir esto antes que dejar que lo descubras después. Las pruebas cubren las reglas de decisión — quién puede ver qué, qué puede salir, qué debe cumplir una entrega. No hacen mágico el resto del software, y no afirmamos que lo hagan. Esa honestidad es el trato, y es todo el trato.

Adónde ir después

• El recorrido completo — construye el frontend y comprueba cada fila de su tabla de verdad incluida.
• El catálogo — el resto del estante, cada pieza re-derivable de la misma manera.
• Ghillie — el asistente al que sirven estas reglas.
• La máquina del Arrecife — qué hardware necesitas si quieres ir más allá de esta página.

Si no funcionó, eso es un hallazgo y nos gustaría saberlo. Una negativa que no puedes explicar nos interesa más que un éxito.