I have spent a long time using alternative languages. I'm a compiler geek. However, most of these languages ultimately lead to disappointment. Not because they necessarily fail, but rather because the problem of writing software is not a problem of language or platform. It is a problem of thought and abstraction. So, the big promises that these new languages and platforms make will ultimately only be fulfilled for a subset of applications. The rest of the time, we must still trudge through the process of good design, good testing, and good real-world feedback.
People love to beat up on C, because it does not have feature X or feature Y, and because there is plenty of bad C software to point at. However, it isn't the language that leads to bad software. Any entrenched popular language has plenty of bad software examples, and plenty of security vulnerabilities. The problem isn't the language, but rather, the developer. A good developer who understands and appreciates the problem can write good software in machine code, C, C++, Rust, Java, Haskell, C#, Go, D, or any other language or platform. A good developer who understands secure programming processes can write secure software in any of these languages, given enough time.
What these higher-level languages offer is better abstraction, which can make time-to-market faster. However, in a deeply entrenched system that is already in market, maintaining the current languages and platforms is typically the better play. This is especially true when the source code is as meticulously maintained as it is with OpenBSD. Someone who understands the basics of C can easily read the OpenBSD kernel or userland, and understand everything about how a given program works. Some knowledge of BSD Make, Bourne shell, Korn shell, and Perl may be required to understand the init scripts and build process, but in all, it is a system that is easy to understand, easy to maintain, and with an excellent development process in place to deliver two builds a year. OpenBSD isn't broke, and a new language isn't going to fix it.
That being said, there are tools that the OpenBSD team could use that neither impact the build time nor require adopting fad language of the week. There are excellent model checkers out there for C, and quite a few proof assistants are gaining the ability to check proofs on C code directly, using Separation Logic and Hoare triplets. These tools can complement an entrenched C system by providing an external mechanism of verification that allows designers to formally verify that implementation meets specification. While formally verifying all of OpenBSD would be a tall order, taking hundreds of man years, formally verifying critical pieces of the kernel and creating simplified contract boundaries for the remaining code would be an excellent complement to the code review process that the OpenBSD team already does. Better still, it is something that could pay off without reinventing OpenBSD to match the current fad, as such verification can be run independently of the standard build process. If I were to make a suggestion to the OpenBSD team, it would be to explore such tools. But, to de Raadt's point, such a suggestion would only be valid if someone did the heavy lifting to put such a tool in place, and if it were of utility to the team. They won't adopt something for the sake of that thing, but they are keen for anything that can practically improve the security of their system.
You're missing high-level languages such as Modula-2 or Free Pascal that are safe-by-default while being close to the machine. They compile faster. They're easier to analyze. Someone who understands C could easily port it to one of these languages or even write a translator that converts them to C for easy integration of incrementally-rewritten pieces of the OS. They don't because they like C for non-technical reasons or want to do one piece of tooling work over another.
Another you might find interesting in alternate history where C programmers adopt better tech is Cyclone that tried to stick to C as much as possible. Rust's safety scheme took a lot of inspiration from Cyclone.
" There are excellent model checkers out there for C, and quite a few proof assistants are gaining the ability to check proofs on C code directly"
I agree. Further, just using Design-by-Contract with property-based and fuzz testing on those contracts would improve things by itself. There was also an academic who applied Frama-C to one of their smallest, battle-tested components in I think a string library. Although no coding flaw found, the exercise did show the documentation was incorrect. Gotta wonder what benefit might happen for less obvious stuff than string operations.
Cyclone is an interesting example. Something that is backward-compatible with C and does not incur significant compile-time overhead, like C++ does, is a potential alternative. Unfortunately, Cyclone was abandoned. It only has support for 32-bit architectures, and it is not being actively maintained. One of the biggest reasons why C is so popular is that it works on practically every platform, even those that Cyclone, Modula-2, and Free Pascal do not.
Of course, if OpenBSD eliminates support for a bunch of the platforms it currently supports, such alternative languages become viable. However, the OpenBSD team purposefully maintains these platforms because they expose errors that would otherwise be missed by a scaled-down release. Software errors missed in x86_64 or x86 may be picked up in MIPS or SPARC because of endianness.
An alternative that I think is more tenable is a language that compiles to C. Such a language can piggy-back off of C's incredible market penetration while adding safety features. Barring some extensions to Cyclone, most of Cyclone's features, for instance, could be implemented as a source-source compiler that targets ANSI C99 or ANSI C11.
Ill be replying to followups on that later tonight or in the morning. I totally agree it should be default. I'll go further to say it should have C datatypes/sizes, calling convention, FFI with little to no annotations required, and compile to C. Each check should be removable per midule with a compiler option, pragma per module, or equivalent keyword/operator marked unsafe . It also needs inline ASM. For its own advantages, add macros, safe linking, and a REPL with incremental compilation.
That by itself would be better and faster to develop than with C with seemless integration with legacy codebases. Side benefit like in my Brute-Force Assurance method would be it benefiting from all tooling C ecosystem has to offer esp static analysis and certifying compiler.
OpenBSD does not have the Bourne shell. One gets the C shell, the Korn shell, and the Korn shell in POSIX mode: no Bourne shell; nor Bourne Again shell.
It is interesting to note that in FreeBSD Perl was removed from the base operating system about a decade and a half ago. So there's apparently an argument to be had that knowledge of Perl need not be required. (-:
People love to beat up on C, because it does not have feature X or feature Y, and because there is plenty of bad C software to point at. However, it isn't the language that leads to bad software. Any entrenched popular language has plenty of bad software examples, and plenty of security vulnerabilities. The problem isn't the language, but rather, the developer. A good developer who understands and appreciates the problem can write good software in machine code, C, C++, Rust, Java, Haskell, C#, Go, D, or any other language or platform. A good developer who understands secure programming processes can write secure software in any of these languages, given enough time.
What these higher-level languages offer is better abstraction, which can make time-to-market faster. However, in a deeply entrenched system that is already in market, maintaining the current languages and platforms is typically the better play. This is especially true when the source code is as meticulously maintained as it is with OpenBSD. Someone who understands the basics of C can easily read the OpenBSD kernel or userland, and understand everything about how a given program works. Some knowledge of BSD Make, Bourne shell, Korn shell, and Perl may be required to understand the init scripts and build process, but in all, it is a system that is easy to understand, easy to maintain, and with an excellent development process in place to deliver two builds a year. OpenBSD isn't broke, and a new language isn't going to fix it.
That being said, there are tools that the OpenBSD team could use that neither impact the build time nor require adopting fad language of the week. There are excellent model checkers out there for C, and quite a few proof assistants are gaining the ability to check proofs on C code directly, using Separation Logic and Hoare triplets. These tools can complement an entrenched C system by providing an external mechanism of verification that allows designers to formally verify that implementation meets specification. While formally verifying all of OpenBSD would be a tall order, taking hundreds of man years, formally verifying critical pieces of the kernel and creating simplified contract boundaries for the remaining code would be an excellent complement to the code review process that the OpenBSD team already does. Better still, it is something that could pay off without reinventing OpenBSD to match the current fad, as such verification can be run independently of the standard build process. If I were to make a suggestion to the OpenBSD team, it would be to explore such tools. But, to de Raadt's point, such a suggestion would only be valid if someone did the heavy lifting to put such a tool in place, and if it were of utility to the team. They won't adopt something for the sake of that thing, but they are keen for anything that can practically improve the security of their system.