Comment by auggierose
1 day ago
> Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code.
What is the difference? You are aware that the code is also only an abstraction, right?
The difference is, that proving something about an abstraction doesn't prove, that you made no mistakes when translating that abstraction into the actual code running, and therefore you have not proven anything of value about the actually running code.
If the abstraction maintains the properties you care about, PROVABLY, there is no problem. As is the case in this case. Again, the code you see in Isabelle is already an abstraction, it is not "running".
> If the abstraction maintains the properties you care about, PROVABLY, there is no problem.
This approach doesn't do that. The translation from the actual executing code to the representation used for runtime analysis is done entirely informally and not checked at all by Isabelle.
6 replies →