Spectre es un nuevo lenguaje de programación diseñado para el desarrollo seguro de sistemas de bajo nivel mediante el uso de contratos. El lenguaje permite definir invariantes a nivel de tipo y precondiciones y postcondiciones a nivel de funciones, ofreciendo seguridad a través de inmutabilidad por defecto. Los contratos se evalúan en tiempo de compilación cuando es posible; aquellos que no pueden verificarse se ejecutan automáticamente en tiempo de ejecución. La gestión de memoria es manual, típicamente mediante asignadores de la biblioteca estándar como Arena o Stack, aunque también soporta asignadores personalizados. Spectre compila desde código de alto nivel a QBE IR, con backends experimentales para LLVM y C99. Incluye una funcionalidad llamada –translate-c que permite migración de proyectos existentes en C al equivalente en Spectre. El lenguaje introduce la palabra clave trust para operaciones impureas o potencialmente inseguras, como la entrada/salida, requiriendo confirmación explícita del programador. Esta propuesta busca llenar un vacío existente en lenguajes de programación basados en contratos que exijan corrección a bajo nivel.
Spectre: lenguaje con contratos para desarrollo seguro de bajo nivel
