takibi

Takibi es un prototipo de investigación que consiste en un lenguaje de sistemas personalizado y un kernel monolítico correspondiente. El proyecto tiene como objetivo eliminar los fallos comunes a nivel de kernel —como desbordamientos de búfer, fugas de recursos y violaciones de contexto— codificando estas obligaciones directamente en el sistema de tipos. Las características técnicas clave incluyen: - Diseño del Lenguaje: Implementa tipos de refinamiento para índices de arrays probados, propiedad afín y lineal para la gestión de recursos, y un sistema de efectos para rastrear contextos de ejecución (por ejemplo, contextos de bloqueo frente a contextos de interrupción). - Compilador: Escrito en OCaml y utiliza LLVM 19 para la generación de código nativo. - Capacidades del Kernel: El kernel es compatible con Linux-ABI, lo que le permite ejecutar binarios ELF de AArch64 existentes. Soporta un subconjunto de syscalls de Linux, tablas de páginas de crecimiento bajo demanda, copy-on-write y un sistema de archivos raíz ext2. - Redes: Incluye su propia pila TCP/IP que soporta ARP, IPv4/IPv6, ICMP y TCP. - Soporte de Hardware: Arranca en QEMU/AArch64 y Raspberry Pi 5, siendo capaz de ejecutar Alpine BusyBox y servir archivos a través de HTTPd. El proyecto sirve como un vehículo de investigación para explorar cómo se puede evolucionar un lenguaje para resolver problemas reales de programación de sistemas, alejándose de las trampas de tiempo de ejecución hacia pruebas estáticas de corrección.