takibi

Takibi 是一个由自定义系统语言和相应单体内核组成的研究原型。该项目旨在通过将相关义务直接编码到类型系统中，消除常见的内核级故障，例如缓冲区溢出、资源泄漏和上下文违规。 关键技术特性包括： - 语言设计：实现了用于证明数组索引的精化类型（refinement types）、用于资源管理的仿射（affine）和线性（linear）所有权，以及用于跟踪执行上下文（例如阻塞上下文与中断上下文）的效应系统（effect system）。 - 编译器：使用 OCaml 编写，并利用 LLVM 19 进行原生代码生成。 - 内核能力：该内核与 Linux-ABI 兼容，能够运行现有的 AArch64 ELF 二进制文件。它支持部分 Linux 系统调用、按需增长的页表、写时复制（copy-on-write）以及 ext2 根文件系统。 - 网络：包含自有的 TCP/IP 协议栈，支持 ARP、IPv4/IPv6、ICMP 和 TCP。 - 硬件支持：可在 QEMU/AArch64 和 Raspberry Pi 5 上启动，能够运行 Alpine BusyBox 并通过 HTTPd 提供文件服务。 该项目作为一个研究载体，旨在探索如何演进一种语言以解决现实世界的系统编程问题，将内核从依赖运行时陷阱转向静态正确性证明。