deft es un módulo para el lenguaje de programación Janet que añade comprobaciones de tipo opcionales aplicables en tiempo de ejecución, en compilación o con anticipación (ahead-of-time). El proyecto aplica los principios del tipado gradual descritos por Siek y Taha, junto con el cálculo de culpa (blame calculus) de Wadler y Findler, lo que permite la interoperabilidad entre código tipado y dinámico dentro del mismo programa.
El sistema incorpora tipos dependientes de predicado (al estilo NQ-Dependent, sin cuantificadores Π ni Σ), tipos compuestos —uniones, intersecciones, ADTs suma sin etiquetar y tipos contenedor—, registros tipados (structs), contratos de orden superior sobre funciones e inferencia bidireccional con unificación. Las anotaciones aparecen en los límites de las llamadas: argumentos al entrar a una función (culpable, el llamante) y valores de retorno al salir (culpable, la función). Tanto los chequeos en frontera como la verificación estática pueden activarse o desactivarse de forma programática.
Deft se integra con Janet mediante el gestor de paquetes jpm —instalación directa, dependencia en project.janet o clonación desde el repositorio en Codeberg— y se importa con un prefijo opcional. Su macro define unificada reemplaza el uso combinado de defn, deftfn, var, ~def y deftval, ofreciendo un tránsito gradual entre código sin tipos y código tipado. La declaración deftype permite crear nuevos tipos a partir de predicados o como combinaciones lógicas de tipos existentes, lo que facilita aproximar uniones, intersecciones y tipos negados sin abandonar la flexibilidad dinámica de Janet.
