| This isn't really the point I'm responding to. I am responding to this idea: > If you are relying on testing for correctness, you have already lost. In any language. As Dijkstra noted, testing can only prove a program wrong. The way to get correct programs, in any expressive-enough language, is by construction. At each level, do only operations that are well-defined by the level below. Expose only well-defined operations to the next level up. I believe this idea is naïve. CPUs contain undocumented instructions, and they expose implementation details via speculative execution and timing attacks. So... by this metric, we have already lost. I think I also take issue with the idea that there is a stable C++ dialect. GCC, Clang, and MSVC have always disagreed on how they interpret the C++ standard. If you want portable code, there is no substitute for testing your program with every compiler you support and on every architecture you support. Proofs won't save you and the standard won't save you, because both proofs and the standard assume that we started from a bug-free foundation that doesn't actually exist. |
You don't seem to realize that testing and proofs are just two faces of the same thing. A test is just an empirical proof of something. Both are rooted in the same logic and assumptions. In fact, in some cases, a test can be exhaustive and then it's as good as a proof. Tests usually have the disadvantage of being inexhaustive, and having to work their logic within the language.
I'm getting to the point that security software, such as an OS kernel, that is vulnerable to timing and speculative execution attacks, is that way not only in spite of being proven, but in spite of testing also.
It's not the case that proofs will fail to reveal that problem, but testing will.
No amount of testing will reveal a problem missed by proof methods, if both the testing and proving are rooted in the same false assumptions.
(Assumptions like "the hardware's protections mechanisms are sound, so that no data flows are observable to an unauthorized domain, so we just have to test the software itself is good.")