I gave a talk at the Koedo LUG / TLUG Software Freedom Day, 2026-09-19 about Takibi, a language I am building together with a Linux-compatible kernel written in it. The slides are below. This post is the longer version of the argument, because fifteen minutes is enough to show three examples and not much else.
Last time I presented this project, at OCaml Meeting 2026, I spent most of the slot on the language implementation, because that is what the room had come for. It was the wrong emphasis. The interesting part of this project is not that a compiler is written in OCaml; it is that writing the language and the kernel at the same time lets you move kernel defects into the compiler. A room full of Linux users is a much better audience for that claim, so this time I built the talk around it.
The Linux kernel is an excellent base to build on. That is precisely why its implementation language matters: C gives a kernel complete control and almost no proof, and in a kernel there is nothing above you to catch what goes wrong. A bad access in an application raises an exception the runtime unwinds. A bad access in a kernel corrupts something and keeps running.
The obvious objection is that people already know this and are already doing something about it. They are. So before claiming a gap, I went looking for what fills it:
| Implementation | Linux ABI layer | What is underneath |
|---|---|---|
| FreeBSD Linuxulator | C, kernel mode | FreeBSD kernel, C |
| gVisor Sentry | Go, userspace | a Linux kernel, mostly C |
| Fuchsia starnix | Rust, userspace | Zircon, C/C++ |
| Asterinas | safe Rust, standalone kernel | a small unsafe Rust TCB (OSTD) |
I find this table encouraging rather than discouraging. It proves the Linux interface is replaceable – that reimplementing it is a thing people successfully do, not a fantasy.
An earlier draft of this post claimed the memory-safe implementations all run on somebody else’s kernel and the bare-metal ones are all C. Asterinas falsifies that, and I am glad it does: a clean-slate kernel in safe Rust with a small audited unsafe core is exactly the direction this whole argument says is right.
So the position I am actually standing in is narrower than “nobody is doing safe kernels”. It is this: every one of these implementations takes its language as given. Asterinas is as safe as Rust can make a kernel, and when it meets a kernel invariant Rust cannot express – a handler that must not reach a sleeping call, an index that must be proved rather than checked – it has the same options everyone else has, which are a lint beside the compiler, a runtime check, or a comment. Changing the language is not on the menu. It is on mine, and that is the only thing here that is unusual.
A language designed on its own cannot know what a kernel needs to prove. A kernel written in someone else’s language cannot ask for a check that language does not have. Build them together and each one keeps telling you what the other is missing – the kernel produces a defect, and the question becomes whether the type system could have refused it.
This is only affordable because of generative AI. I am one person, and a compiler plus a kernel is not a one-person project on a normal budget. The AI is the method; it is not the point, and I deliberately kept it to one slide.
The talk showed three defect classes that Takibi rejects at compile time. I picked them against a deliberately harsh bar: neither C nor Rust refuses this when the program is built. The bar did real work – it threw out candidates I liked.
A blocking call inside an interrupt handler. A handler runs with interrupts masked, so a function it reaches that sleeps is waiting for an event that can no longer arrive. What makes this a defect class rather than a coding tip is the distance: the handler calls a helper, which calls a logging routine, which spins on a UART ready bit. Every function on that path is correct in every other caller. Takibi’s !{interrupt} roots reject a transitively reachable may_block, and the diagnostic names the whole path – including the middle function, which declares nothing at all.
Linux does detect this, at run time, through might_sleep(). That requires CONFIG_DEBUG_ATOMIC_SLEEP, which production kernels do not ship, and it only fires if the path actually executes.
A handle that may name a destroyed object. Kernels refer to objects by handle – a slot index, usually with a generation counter. A handle is plain data, so it survives the destruction of the thing it names. A pid is this same handle with the generation left out, which is why the instance every Linux user has met is pid reuse: between looking up a pid and acting on it the process can exit, the number is handed to a new one, and the signal lands on a stranger. Linux answered that not with a language change but with a new kind of handle, pidfd. A generation is the cheaper repair and makes the reuse detectable, but only by a comparison somebody remembered to write, on every lookup. The general case is harder than the pid case, because the call that destroys the object usually does not take the handle as an argument at all, which is why reading the caller reveals nothing. Takibi marks the functions that can destroy a given handle type and kills the binding at the first call that reaches one, unless a live witness vouches for it.
An unproven index that leaves a trap in the kernel. An index arrives from a packet or an MMIO read and addresses a table. There are exactly three possible outcomes in a shipped binary: nobody checks and memory is corrupted; somebody checks at run time and the failure becomes a trap, which on bare metal ends the core; or the question is settled before the binary exists. Takibi’s refinement types take the third, and --forbid-trap turns every remaining unproved site into a compile error. The whole maintained kernel is built that way. It contains no bounds-check trap because no access needed one, not because the checks were disabled.
Two more entries did not fit in fifteen minutes and are worth reading if this kind of thing interests you. An exception frame that does not match the entry sequence is my favourite, because it is the one case where C and Rust are not merely unequal to the task but absent from the conversation: in both, the frame layout is a struct in one file and an assembly stub in another, and the compiler is never shown both. Takibi’s exception_entry is a language construct that emits the save sequence, so the compiler can tell you exactly which register your struct left out. A wire-endian field used as a host integer is the weakest claim of the five and I label it as such in the catalog: C has sparse’s __bitwise, Rust has crates like zerocopy, and both genuinely work. The difference there is not capability but where the check lives – in Takibi it is the field type of a packed struct, so there is nothing to opt into and nothing to install.
I also threw one candidate out for failing the bar: constructing an MMIO pointer requires unsafe in Takibi, but it requires unsafe in Rust too, so there is no claim to make.
This is the question I actually get asked, so let me answer it without being rude about Rust, which is a good language doing good work.
Rust for Linux is right, and it is working. But it inherits Rust’s ceiling. Rust has no type-level effect for atomic context, which is why Rust for Linux built klint, an out-of-tree MIR lint that tracks preemption count. Worth being precise about that one: klint is a compile-time check, so this is not Rust failing to catch the bug. It is the property living in a separate analysis rather than in a function’s type, so it does not travel with a signature and is enforced only where that tool is run. The borrow checker reasons about references, so a slot-plus-generation handle has no lifetime to attach. Crates fill that gap and fill it well – slotmap and generational-arena compare a generation on every lookup – but the check happens at run time, it is a property of the crate rather than the language (reach for slab, which hands out bare indices, and the defect is back), and no crate can lift it into the type – the key is Copy, so it duplicates freely and no liveness travels with it.
And on the index: safe Rust genuinely prevents the memory error, and saying otherwise would be false. Two things even happen before run time – a constant index out of range is rejected while compiling, and a check the optimizer can prove redundant is deleted – but neither reaches an index that arrives from a packet. For that one the check is emitted, its failure on bare metal ends the core, the elision is a best effort that nothing fails the build over, and get_unchecked moves the proof obligation into unsafe rather than discharging it.
My worry is not that Rust is insufficient. It is that “Rust exists, so let us improve kernel safety as far as Rust reaches” is a ceiling nobody notices they are standing under. Somebody should go and look at what is above it, and a self-made language is a cheap way to look: nothing depends on it, so it can be broken and rebuilt every week. If something found up there eventually turns up in Rust or Zig, that is the best ending this project could have. I would like to be ground that someone else builds on, not a replacement for anything.
A page that transcribes a program and the error message it produces is a claim with no verifier, and a stale page renders exactly like a true one. Since the whole point is to be checked by strangers, the build checks it first: check_wont_compile_catalog.py verifies that every entry names a test case that really exists in the suite and that the index agrees with the entries, and buildcheck_wont_compile_samples.py compiles every program printed in the catalog with the compiler that build just produced – eight must be rejected with the exact message printed beside them, five must be accepted.
So a compiler regression does not quietly make the documentation wrong. It makes the build red.
Which means you do not have to take my word for any of this. Copy a program out of the catalog, run it through the compiler, and see whether you get the message I said you would.