2 ms·
> have a solid system for validating that two pieces of code are equivalent according to the C abstract machine What ideas do you have for doing that in anythi
by JonChesterfield 4y ago
> have a solid system for validating that two pieces of code are equivalent according to the C abstract machine
What ideas do you have for doing that in anything under exponential time?
- mort96 4y agoI don't have any, I haven't thought about it enough. However, the reason I think it might be interesting is that checking if something is a correct solution is often easier than coming up with a correct solution for a lot of classes of problems (assuming P!=NP and all that). And maybe you can't make a polynomial time verifier which works in the general case, but maybe you can make a useful one which handles a lot of cases.
- c-cube 4y agoI'm pretty sure that program equivalence is undecidable, ie you literally can't write this validation pass at all. There's a C compiler (compcert) that is formally verified to preserve the semantic of its input C code down to assembly, but it takes a lot of human developed proofs in Coq to get there.