I love OpenBSD and use it a lot. But this notion of C everywhere for everything is wrong.
This isn't an issue of language or platform, but an issue of process. The OpenBSD team has one of the best overall software development processes out there, but it is still very much a manual process. The class of exploits that are currently being discovered are often discovered via tool-assisted analysis. Such tools can also be used during the software development process to find errors that can be exploited. There are a dozen or so of such tools available for C currently ranging from OSS to commercial. Typically, these tools rely on model checking or bounded model checking, and they are quite effective at reducing attack surfaces or entire classes of errors beyond what most languages can provide on their own.
To take full advantage of model-guided development, however, requires a different software development process that is more difficult to adapt to older code bases overnight. Still, this adaptation is significantly less effort than, say, porting a C code base to Go or Rust. Model-guided development and other types of formal methods aren't silver bullets, and they aren't perfect. But, they are much more effective tools for building better systems than a language or compiler on its own.
I suspect that the OpenBSD developers will adapt to using a model-guided approach. They make use of some static analysis tools already. I find this much more likely than the OpenBSD team switching to Go or Rust, as it is a much more pragmatic solution and a more powerful solution.
I am skeptical of the claim that it is more "pragmatic" to adopt formal methods to achieve memory safety, as the number of projects that achieve memory safety through formal methods is multiple orders of magnitude smaller than the number of projects that achieve memory safety through just writing in a memory-safe language.
OpenBSD, AFAIC, has not announced any plans. But, there are plenty of tools out there that work. CBMC is a solid example and it is one I have used to great success with both systems programming and firmware development. As noted, this requires both a process change and a use of this tooling. Properly using assertions is a skill, but it can typically be cross-checked using existing manual processes with the added benefit of catching logic issues like the one that caused this RCE.
Which tools would I start googling if I wanted to learn more about this?
Rewriting the world in some safe language isn't a panacea, this meme is getting very old.
