|
|
|
|
|
|
by fluoridation
16 days ago
|
|
|
>If you write code in Lean 4 or Idris 2, you may not completely understand why it is or isn't correct, but their respective compilers will certainly prove it to you one way or the other. No, the prover can only prove that the implementation matches the formal language specification. That's different from the application being correct. |
|
|