2 ms·
Lean is like a statically typed programming language and validity is guaranteed if it compiles. The only room for errors is in translating a non-Lean theorem in
by twiceaday 28d ago
Lean is like a statically typed programming language and validity is guaranteed if it compiles. The only room for errors is in translating a non-Lean theorem into Lean, so that you are not proving what you think you are proving.
- throw-qqqqq 27d agoGreat explanation. I’ve heard this referred to, as The Formal Specification problem. From https://en.wikipedia.org/wiki/Formal_specification#Limitations https://en.wikipedia.org/wiki/Formal_specification#Limitatio... > A design (or implementation) cannot ever be declared “correct” on its own. It can only ever be “correct with respect to a given specification.” Whether the formal specification correctly describes the problem to be solved is a separate issue.