43 ms·
The 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
by vilhelm_s 13y ago
The 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).