[kazinator]

Erratum: testing, of course, exercises every layer you depend on, whereas proof methods typically assume that the things below conform to their contracts. That is where proofs are weak. A proof will show that your code is correct; a test will reveal a compiler bug, CPU bug, faulty RAM, ...

[orneryostrich]

Oh! This erratum is the point I’ve been trying to get across. It sounds like we agree on this?