takibi

Takibi est un prototype de recherche composé d'un langage de systèmes personnalisé et d'un noyau monolithique correspondant. Le projet vise à éliminer les défaillances courantes au niveau du noyau — telles que les dépassements de tampon, les fuites de ressources et les violations de contexte — en encodant ces obligations directement dans le système de types. Les principales caractéristiques techniques incluent : - Conception du langage : Implémente des types de raffinement pour des indices de tableaux prouvés, une propriété affine et linéaire pour la gestion des ressources, et un système d'effets pour suivre les contextes d'exécution (par exemple, contextes bloquants vs contextes d'interruption). - Compilateur : Écrit en OCaml et utilise LLVM 19 pour la génération de code natif. - Capacités du noyau : Le noyau est compatible Linux-ABI, ce qui lui permet d'exécuter des binaires ELF AArch64 existants. Il prend en charge un sous-ensemble d'appels système Linux, des tables de pages à croissance à la demande, le copy-on-write et un système de fichiers racine ext2. - Réseau : Inclut sa propre pile TCP/IP prenant en charge ARP, IPv4/IPv6, ICMP et TCP. - Support matériel : Démarre sur QEMU/AArch64 et Raspberry Pi 5, capable d'exécuter Alpine BusyBox et de servir des fichiers via HTTPd. Le projet sert de vecteur de recherche pour explorer comment un langage peut évoluer pour résoudre des problèmes de programmation système du monde réel, en s'éloignant des pièges d'exécution vers des preuves statiques de correction.