takibi

Takibi é um protótipo de pesquisa composto por uma linguagem de sistemas customizada e um kernel monolítico correspondente. O projeto visa eliminar falhas comuns em nível de kernel — como buffer overflows, vazamentos de recursos e violações de contexto — codificando essas obrigações diretamente no sistema de tipos. As principais características técnicas incluem: - Design da Linguagem: Implementa tipos de refinamento para índices de array comprovados, ownership afim e linear para gerenciamento de recursos, e um sistema de efeitos para rastrear contextos de execução (ex: contextos de bloqueio vs. interrupção). - Compilador: Escrito em OCaml e utiliza LLVM 19 para geração de código nativo. - Capacidades do Kernel: O kernel é compatível com Linux-ABI, permitindo a execução de binários ELF AArch64 existentes. Suporta um subconjunto de syscalls do Linux, tabelas de páginas com crescimento sob demanda, copy-on-write e um sistema de arquivos raiz ext2. - Networking: Inclui sua própria pilha TCP/IP com suporte a ARP, IPv4/IPv6, ICMP e TCP. - Suporte de Hardware: Inicializa no QEMU/AArch64 e Raspberry Pi 5, sendo capaz de executar Alpine BusyBox e servir arquivos via HTTPd. O projeto serve como um veículo de pesquisa para explorar como uma linguagem pode evoluir para resolver problemas reais de programação de sistemas, afastando-se de traps de runtime em direção a provas estáticas de correção.