Show HN: Lungo Generates Rust, Python, from Lean Proof Source

Category: devtools

Tags: lean4, transpiler, code-generation, formal-verification, multi-language

Score: 7.0/10 (Innovation: 8, Technical: 7, Documentation: 4, Utility: 6)

Lungo is a tool that transpiles Lean 4 programs to Rust, C, Go, Python, Swift, and TypeScript, using Lean's proof and type checking to verify correctness before generating idiomatic APIs in each target language. It is interesting because it leverages Lean's formal verification capabilities to produce multi-language output from a single source, potentially bridging verified logic with practical language ecosystems.

Target audience: backend developers, language tooling engineers, formal methods researchers

Repository: https://machinefabric.com/lungo/

View on Hacker News