Re:AlphaProof Code
by cortesoft on Tuesday November 10, 2026 @11:23AM
(#50442535)
This is true for all formal verification systems, though. You can only formally prove that code does what a spec says, you can’t verify that a spec perfectly matches what the code is intended to do.
[ Parent
| on HN ]
Well, arguably if you generate your code from the spec itself then it could be possible.
But even then, what's not possible is to "know" whether the spec=code is whatever the creator actually had in mind.
But still, the target programming language's formalism is still likely done on a higher level, than e.g. its compiler output on a given CPU, so compiler bugs could still "throw a wrench" into the system.