Verbose is a small experimental language whose compiler proves properties (like termination) and emits tiny, readable x86-64 — no runtime, no GC, no libc. On a working branch, a rule written in Verbose itself now emits a standalone ELF that runs and prints its result. Here's factorial(5) from source to binary, plus an honest benchmark vs gcc/rustc/go.