corrección del software
explora métodos para comprobar el software escrito por agentes, desde pruebas de propiedades hasta reproducción determinista. lecciones en inglés.
by hraness · drafted with ai assistance
el software que un agente escribe en una tarde cuesta poco producirlo, pero cuesta mucho saber si funciona correctamente. conviene facilitar la detección de errores. cada lección de esta categoría presenta un mecanismo que detecta una clase concreta de error, tomado de los proyectos que mantiene Hraness.
la serie comienza con una definición práctica de programación resistente a fallos y recorre las herramientas: demostraciones formales, pruebas con estado, pruebas de propiedades, mutación, registros de afirmaciones, reproducción y mecanismos de publicación que permiten verificar el origen de los archivos. cada lección enlaza los proyectos que usan la técnica y explica qué no puede demostrar.
las lecciones están en inglés. la introducción es de acceso libre; las demás requieren suscripción.
lecciones
- programación resistente a fallos: una definición práctica (en inglés)empieza aquí. impedir que se representen estados inválidos y facilitar la detección de errores
- Lean: demostrar que las cuentas cuadran antes de ejecutar las pruebas (en inglés)suscriptores. un verificador de demostraciones como paso de compilación
- TLA+: comprobar las intercalaciones que una prueba no alcanza (en inglés)suscriptores. errores causados por el orden de los eventos
- hegel: pruebas con estado que detectan el error de tres pasos (en inglés)suscriptores. provocar un fallo entre commit y fsync, y después recuperarse
- pruebas de propiedades: analizadores, proyecciones y conversiones de ida y vuelta (en inglés)suscriptores. enunciar una ley y generar entradas que intenten incumplirla
- Kani: comprobar cada número que puede recibir una función (en inglés)suscriptores. verificación acotada de modelos para la aritmética que las pruebas solo muestrean
- registros de afirmaciones: anotar lo que quedó sin demostrar (en inglés)suscriptores. relacionar cada promesa con su evidencia y su fecha
- errores introducidos a propósito: cómo poner a prueba las pruebas (en inglés)suscriptores. introducir un error y comprobar que las pruebas fallen
- estados inválidos: tipos, Result y análisis de datos unknown (en inglés)suscriptores. tipos que excluyen valores incorrectos y analizadores en cada punto de entrada
- dos implementaciones, una especificación: usar la paridad como oráculo de pruebas (en inglés)suscriptores. si TypeScript y Rust discrepan, existe un error o una laguna en el contrato
- reproducción sin relojes: ejecuciones deterministas como evidencia (en inglés)suscriptores. poder repetir una ejecución permite depurarla
- Direct: cada pantalla por URL, de forma determinista (en inglés)suscriptores. datos fijos en una URL estable producen la misma pantalla cada vez
- StyleX: un sistema de diseño tipado para todos los sitios (en inglés)suscriptores. CSS en tiempo de compilación con la paleta del conjunto de productos
- publicaciones que permiten verificar su origen (en inglés)suscriptores. evidencia firmada del commit, el flujo de trabajo y la ejecución que creó cada versión
- Rust en los núcleos donde la seguridad de memoria es crítica (en inglés)suscriptores. Rust donde un error de memoria corrompe el estado; TypeScript donde el riesgo está en la lógica
proyectos
- algal (en inglés)organismos cuyas ejecuciones generan comprobantes que puedes reproducir sin conexión, byte por byte.
- gobstopper (en inglés)un archivo local de sesiones de agentes con demostraciones sobre sus transcripciones.
- vhalla (en inglés)salas entre pares con especificaciones, mutantes y entrega verificada por cuórum.