[orneryostrich]

You do know that every operating system and CPU in existence has ill-defined operations, right?

The best-defined software I know of is SQLite. Every function is carefully documented with a description of all failure modes and returned error codes.

But also... SQLite has one of the most comprehensive test suites in existence, so I guess they lost? https://www.sqlite.org/testing.html

[ncmncm]

SQLite is coded in C. Correct-by-construction was not among the choices available.

SQLite are in a good position to switch to building with a C++ compiler, and then modernize incrementally. They won't, for cultural reasons. They probably could use that C-to-Rust translator thing that was used on Quake3, but they won't do that either, for better reasons.

[orneryostrich]

C++ is even less well-defined than C, though. We find defects in the standard and inconsistencies between Clang/G++/MSVC every day.

You’re demanding a rigor that is not possible with a modern technology stack.

[kazinator]

In a greenfield project, you can restrict the code base to stable C++ dialect (all the way back to C++98 if necessary), and you can dictate the use of C++ features which make it safer than C. For instance, smart pointers for all memory allocation.

[orneryostrich]

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.

[kazinator]

If you use undocumented instructions, you're not following "do only operations that are well-defined by the level below". The existence of undocumented instructions doesn't invalidate the concept of correctness by contract.

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.")

[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, ...