Archived: a snapshot from October 2026, kept as written. nanofil has moved on (it now requires Fil-C 0.687); nanofil's page lists what is current.
nanofil: where it stands
nanofil is a C compiler written in Prolog that emits Fil-C code: x86-64 assembly in which every pointer carries a capability, every access is checked, and the collector sees every pointer. Its objects link with filcc's, the clang-based Fil-C compiler. This page says what it can do today and what it costs, as far as we have measured.
-O, geomean of 11 workloads-O, for SQLiteWhat it is
The pipeline is ordinary in shape: preprocess, parse, type, lower to an IR of Prolog terms, optionally optimize, then pizlonate (insert Fil-C's checks, as filcc's LLVM pass does), validate, and emit assembly. Two things are unusual.
- The IR has a meaning you can run. An interpreter defines what each instruction does, including what happens when a check fails. Tests compare that meaning against the native code and against filcc's programs.
- Safety rests on one validator. After pizlonation, a checker re-derives every fact a check depends on: which values are pointers, which proofs are still valid, where the collector may run. The optimizer can be wrong; if its output would be unsafe, compilation stops. A code review in October 2026 tried to break that and found no way through.
The point of the project is a compiler whose safety argument can be read and worked on directly, not a faster Fil-C. You can read its source drawn as terms or run it in your browser.
What it can build
nanofil accepts C17 with the GNU extensions real packages use: statement expressions, typeof, __attribute__((cleanup)), computed goto, VLAs, transparent unions, weak symbols and aliases, .symver, K&R definitions, C11 atomics and setjmp. Unknown attributes are refused rather than ignored. The rule throughout is to refuse loudly instead of miscompiling.
The survey builds every C package in filnix's port list with nanofil in place of the compiler. Of the 200 that filcc builds, nanofil builds 160, compiling about 44,900 objects with no fallback to clang. The 60 among them whose ports run tests pass them, as filcc's builds do. They include GTK 3, GLib, SQLite, CPython, Lua, bash, coreutils, gmp, libsodium and netcdf. With -O it built 154, and the four -O-only failures have since been fixed. With vector types turned on (--vectors, still opt-in) eight more build, among them xz, x264, zstd, libtiff and Ghostscript.
Sixteen workload checks build programs like bash, CPython, SQLite, coreutils, xz and jq with nanofil, plain and with -O, and require their output, and often their own test suites, to match filcc's builds, also under the collector's stress mode.
What stops the other 40, roughly in order. emacs and libgcrypt are left out of the survey as slow builds and timed separately.
| Cause | Packages | Examples |
|---|---|---|
Vector types and SIMD intrinsics (eight of these build with --vectors) | 17 | fftw, gtk4, libwebp, x264 |
Assorted syntax and typing gaps: __int128, complex literals, glibc's link.h | 9 | mbedtls, nss, systemd |
| Missing builtins and unresolved Fil-C symbols at link | 7 | bison, gnutls, libaom |
| Inline assembly that filcc checks and runs natively | 3 | openssh, openssl |
| Constant folding, alignment, a timing-dependent test | 4 | libffi, libcdio, libressl |
The full table is in survey.md.
How fast its code runs
The benchmark gate runs eleven workloads: zlib, bzip2 and lz4 compressing and decompressing 4 MiB, three Lua scripts, and an SQLite session with joins, window functions, JSON and full-text search. Each nanofil build must print exactly what filcc's does; then each runs seven times, pinned to one core. Ratios are run time against filcc -O2; lower is better. The plain column is from an earlier measurement over ten of the workloads.
| Workload | plain | -O | |
|---|---|---|---|
| zlib -6 | 8.5× | 2.2× | |
| bzip2 -9 | 9.4× | 1.6× | |
| lz4 -d | 14× | 2.4× | |
| Lua, strings | 11× | 1.4× | |
| SQLite | — | 1.8× | |
| Geomean, all eleven | ~11× | 1.8× |
Plain nanofil keeps every value in a stack slot and checks every access: it exists to be obviously right. -O adds inlining of small functions, a cheap middle end, register allocation (pointers included) with a checker that verifies the allocation, better branches, small inline copies and check renewal, which reuses a proven check when the same pointer is checked again; it went from 4.6× to 1.8× over two rounds of work, and every step is checked against the plain path.
The remaining gap is mostly deliberate. filcc merges and hoists checks out of loops; nanofil runs every check where the C access is, so a bad access traps at the same place and with the same message. Moving checks safely needs a separation of spatial and temporal proofs that is still being designed. Calls into the runtime and libc are the next largest share, and they cost the same in filcc's builds. The full account is in perf.md.
How fast it compiles
SQLite's amalgamation, sqlite3.c: 266,000 lines, 123,000 after preprocessing. Measured on one machine (Ryzen 9 7950X3D) while it was also running other builds, so treat the numbers as rough; the ratios between them held in earlier quiet runs.
| Compiler | Time | Peak memory | Object |
|---|---|---|---|
| filcc -O0 | 54 s | 1.8 GB | — |
| filcc -O2 | 139 s | 1.4 GB | 11.3 MB |
| nanofil, plain | 87 s | 1.1 GB | 23.8 MB |
nanofil -O | 210 s | 1.2 GB | 12.2 MB |
So nanofil compiles in the same range as filcc: plain nanofil sits between filcc -O0 and -O2, and -O takes about 1.5× filcc -O2, producing an object of about the same size. Ordinary files compile in well under a second; the saved Prolog state starts in 0.05 s.
The limit that matters is memory, not time. nanofil holds a whole translation unit through every stage, and SWI-Prolog runs with a 1 GB stack. Files with megabytes of initializers, such as GLib's generated resource blobs, or very large amalgamations sit near that limit. Garbage-collector tuning brought SQLite down to 650–800 MB; streaming one function at a time through the back end is the real fix, and it is planned.
What it does not do yet
- C++,
__int128,_Complex, 256-bit vectors, and inline assembly beyond cpuid, rdtsc, fences and pause. 128-bit vector types are opt-in. - Other targets. x86-64 Linux only, as Fil-C itself.
- Its own preprocessor in package builds. nanofil has a preprocessor and tests it, but package builds currently preprocess with filcc's to match its headers and predefined macros exactly.
- A proof. nanofil has executable semantics, a validator, differential tests and bounded symbolic comparisons, not a correctness proof. A Rocq proof that the validator's checks are sound is under way; that is a statement about every valid module, and it does not say any program never panics, which would be a separate theorem per program. A review in October 2026 found attribute-placement bugs in the frontend, such as attributes written in C23
[[gnu::…]]form being dropped. Those places now refuse instead; random differential testing against filcc is next.