4 ms·

Compcert doesn't qualify as a large program?

• pron 10y ago
  No. It's medium-sized; and it required a world expert, and it required a lot of effort, and even he had to skip on the termination proofs because they proved too hard/time-consuming, so he just put in a counter and throws a runtime exception if it runs out.