Lean and Coq might not be the right choice. Perhaps something like Dafny, F*, or Why3, where code and theorems live together. Nevertheless, Lean 4 has closed t

Lean and Coq might not be the right choice. Perhaps something like Dafny, F*, or Why3, where code and theorems live together. Nevertheless, Lean 4 has closed the gap and it's closer to those than Coq at this stage.