Introducing lungo. It treats Lean code as the source of truth. Write your logic in Lean and prove what you claim it does. lungo generates Rust, Go, Python, TypeScript, Swift and C, with the proofs carried into output package as checked claims.
For the past year I’ve toiled to keep CapDAG, my protocol for routing work between capabilities, consistent across five languages with Claude and thousands of cross-impl tests. Between changing core design and varying levels of mirror-parity, it’s been a bruising battle.
So I learned Lean and proved the core instead. lungo just fell out of that and is now used all over MachineFabric making my life so much easier. It takes the output from Lean's own compiler and fits right in without requiring Lean’s runtime or toolchain to run generated code.
lungo ports Lean’s runtime to Rust so the generated code doesn’t require Lean’s toolchain and runs on all OSes and even in the browser(TypeScript + Wasm). The code keeps Lean’s object layout and behaves byte-for-byte identical to Lean’s own executables. All Contributions welcome.
joeharshamshiri•58m ago
For the past year I’ve toiled to keep CapDAG, my protocol for routing work between capabilities, consistent across five languages with Claude and thousands of cross-impl tests. Between changing core design and varying levels of mirror-parity, it’s been a bruising battle.
So I learned Lean and proved the core instead. lungo just fell out of that and is now used all over MachineFabric making my life so much easier. It takes the output from Lean's own compiler and fits right in without requiring Lean’s runtime or toolchain to run generated code.
lungo ports Lean’s runtime to Rust so the generated code doesn’t require Lean’s toolchain and runs on all OSes and even in the browser(TypeScript + Wasm). The code keeps Lean’s object layout and behaves byte-for-byte identical to Lean’s own executables. All Contributions welcome.