Hillel Wayne, autor de "Logic for Programmers" y especialista en métodos formales, ofreció esta charla en la conferencia Software Should Work (SSW) 2026 titulada "How to Find Bugs in Systems That Don't Exist". La presentación introduce los métodos formales, disciplina que usa matemáticas para analizar código y diseños en busca de errores, pero su objetivo real no es enseñar la técnica en sí, sino transmitir las perspectivas e ideas que el ponente ha extraído de ocho años aplicándola y que resultan útiles incluso sin usar las herramientas formales.
Wayne estructura la exposición en torno a cuatro conceptos clave: propiedades (qué significa que un sistema sea correcto, desde aserciones hasta propiedades operativas como gestionar 10.000 solicitudes por segundo); abstracción (cómo modelar sistemas eliminando detalles); verificación (el proceso de asegurar que el modelo cumple las propiedades); y entornos (qué supuestos hacen posible la corrección).
La charla arranca con un ejemplo introductorio de marcado de tareas para ilustrar dos tipos clásicos de errores: un fallo de vivacidad (una tarea queda marcada como hecha sin haberse ejecutado realmente) y una infracción de seguridad (dos ejecuciones concurrentes realizan la tarea dos veces antes de marcar el estado). Wayne traslada estos conceptos a casos reales: un instalador de aplicaciones que corrompía datos al intentar reinstalar algo en proceso, sistemas de envío de paquetes o un comedero automático para gatos. La sesión se grabó con un ligero retraso técnico y dura 38 minutos.