No one can know if it is bug free, that is impractical. But it also isn’t like this is a weekend hobby project either. Most of the bugs that get out are in unimportant peripheral code and integrations.
No one can know if it is bug free, that is impractical. But it also isn’t like this is a weekend hobby project either. Most of the bugs that get out are in unimportant peripheral code and integrations.
I'm quite curious what tools you're using to formally verify your C++ code if you are. My understanding is that in general you can't, which is why msan/asan exist, to get a first approximation of verifying things that can't be formally verified for most C++ code.
(In general, I'm dubious of these claims that "Most serious projects won’t hire you if you aren’t capable of writing memory safe code in your sleep", because I think if you asked the majority of the members of the C++ committee if they could do that, they'd say no).
In many of these systems it is standard practice to generate arithmetically limited types pervasively. This is almost transparent in C++17. While it is possible to verify much of this at compile-time in theory, it almost never is because it isn't worth the effort (C++20 may start to change this) and testing at runtime has proven to be nearly as good. People underestimate what is possible with the C++ type infrastructure in this regard.
This type of software design was originally done because it allows for exceptional performance but has become popular for safety reasons. It uniquely allows you to make guarantees about runtime behavior under diverse adversarial workloads that would otherwise be difficult to make.
Bugs in practice tend to occur at the interface with third-party code, which requires dropping out of any internal type system, or in the form of performance anomalies due to unexpected hardware behaviors interacting with the scheduler design. Logic bugs in the core bits tend to be found in testing.
Presuming that this style works equally well for all software seems presumptuous and perhaps naive, does it not?