2 ms·
There's a very simple solver that completes that goal: one that reports that it cannot prove any code as correct. So there must be a secondary goal of "maximize
by dzaima 3y ago
There's a very simple solver that completes that goal: one that reports that it cannot prove any code as correct. So there must be a secondary goal of "maximize the amount of accepted code", which is a significantly less trivial question.
- TylerE 3y agoYes, exactly. Saying "just do the thing correctly, duh!" is easy. Ya know the saying about the difference between theory and practice?
- Georgelemental 3y agoI guess you have to add an implied "and preserves backward compatibility for (>99.9% of) sound code that compiles today" condition