If you don't use a formal tool like Lean to define your spec, then your C++, Rust, or other implementation effectively becomes the spec.
So “you might get the spec wrong” applies either way. The big difference is that with Lean, you can prove that the implementation matches the spec. With mainstream programming languages, you can't.
deterministic · · focus · HN ↗
So “you might get the spec wrong” applies either way. The big difference is that with Lean, you can prove that the implementation matches the spec. With mainstream programming languages, you can't.