|
|
|
|
|
|
by zitterbewegung
60 days ago
|
|
|
The better look at this is not to prove that you have no bugs is that to prove that a program conforms to a specification that Lean can verify. Even with the addition of two numbers the execution of a program can be wrong if the CPU has a fault or if the runtime of the program has a bug. I think you just need to look at why formal verification exists. |
|
|