2 ms·
What exactly is doing the verification? Another program, no? In which case why would you trust that program any more than the compiler that generated the machin
by dkarapetyan 13y ago
What exactly is doing the verification? Another program, no? In which case why would you trust that program any more than the compiler that generated the machine code? At some point you must trust something to be correct. Whether that's the compiler or something else doesn't really change anything.
- vilhelm_s 13y agoThe idea is to minimize the trusted computing base---a compiler and runtime system for a high level language is a big and complicated system, so it is very hard to get it right, but a proof checker can be small so it is easier to be confident that it is correct. (This idea is also known as the "de Bruijn criterion").
- dllthomas 13y agoIdeally, we should minimize the code in any given path to assurance, but maximize the number of independent paths to assurance (modulo resource constraints).