Об этом проекте

Takibi представляет собой исследовательский прототип, состоящий из специализированного системного языка и соответствующего монолитного ядра. Проект направлен на устранение распространенных сбоев на уровне ядра, таких как переполнение буфера, утечки ресурсов и нарушения контекста, путем кодирования этих обязательств непосредственно в системе типов. Ключевые технические особенности включают: - Дизайн языка: внедрение типов уточнения (refinement types) для доказанных индексов массивов, аффинного и линейного владения для управления ресурсами, а также систему эффектов для отслеживания контекстов выполнения (например, блокирующие контексты против контекстов прерываний). - Компилятор: написан на OCaml и использует LLVM 19 для генерации нативного кода. - Возможности ядра: ядро совместимо с Linux-ABI, что позволяет запускать существующие ELF-бинарные файлы AArch64. Оно поддерживает подмножество системных вызовов Linux, таблицы страниц с динамическим расширением, механизм copy-on-write и корневую файловую систему ext2. - Сеть: включает собственный стек TCP/IP с поддержкой ARP, IPv4/IPv6, ICMP и TCP. - Поддержка оборудования: загружается на QEMU/AArch64 и Raspberry Pi 5, способен запускать Alpine BusyBox и предоставлять файлы через HTTPd. Проект служит инструментом исследования того, как язык может развиваться для решения реальных проблем системного программирования, переходя от ловушек времени выполнения к статическим доказательствам корректности.