alt Hacker NewsIf 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. 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.