3 ms·
Can you explain? When a piece of software is verified with an Agda proof, that is generally a real proof. The proof may not cover all aspects, but in those asp
by Peaker 15y ago
Can you explain?
When a piece of software is verified with an Agda proof, that is generally a real proof. The proof may not cover all aspects, but in those aspects you really do not have bugs.
Perhaps you mean non-proven certification? Or a weak certification of too few aspects?
- chrisjsmith 15y agoI think it was probably a weak certification in this case. They paid for core concerns to be covered, not necessarily the entire toolchain (which TBH is where the problems were - X working with Y properly). In fact I think it was that linker that fluffed stuff. I should modify my comment really.
- regehr 15y agoHistorically, compiler certification is a bad joke. It amounts to concerted testing at best, and wishful thinking in most cases. Few (remotely useful) compilers have been verified in any mathematical sense, and even then there is generally a wide gulf between what is proved and what we would intuitively expect a truly correct compiler to do.
- chrisjsmith 15y agoThis was in the late 90's and it was an ADA compiler so you are probably correct there.