c-cpp-to-lean4-translator
Installation
SKILL.md
C/C++ → Lean 4 Translator
Lean is for when you need a proof, not a check. Dafny asks an SMT solver "is this true?"; Lean asks you to construct the proof term. More work, more control, no timeouts.
When Lean over Dafny
| Situation | Why Lean |
|---|---|
SMT solver times out or returns unknown |
You write the proof steps; no solver to time out |
| Proving mathematical properties (complexity bounds, algebraic laws) | Lean has Mathlib; Dafny has arithmetic |
| The proof itself is the artifact (paper, certification) | Lean proofs are inspectable; Dafny's are solver-internal |
| You need custom proof tactics | Lean is a tactic language; Dafny's hints are fixed |
The functional lift
Lean is purely functional. The translation path is: imperative C → functional model → proof about the model.