> we don’t know how to create a simpler memory safe low-level language. This may well be true, but using a memory-safe language is never, ever the goal. The go

> we don’t know how to create a simpler memory safe low-level language. This may well be true, but using a memory-safe language is never, ever the goal. The goal is creating correct and secure programs -- that have as few bugs and security flaws as possible/required -- as cheaply as possible. While a memory safe language in the style of Rust is one means toward that end, that eliminates an important class of bugs at the cost of language complexity, it is not the best way toward that goal, at least not that we know, and it is certainly not the only one [1]. I.e. the hypothesis that if I want to write a program that's as correct as possible/needed as cheaply as possible then I should necessarily use the language that gives me the most sound guarantees regardless of the cost this entails is just some people's guess. It's hard to say if it's a good guess or a bad one because it's clear that we're talking about specific sweet-spots on a wide spectrum of options that could be very context-dependent, but it's still a guess, with good arguments both in its favour as well as against. > In Rust, there are choices to be made, some important enough to have dedicated syntax. Not only that, but those choices are exposed in the type signature and are, therefore, viral. Changing some internal technical implementation detail can require changes in all consumers. This is not a problem with the type system -- on the contrary, Rust's type system ensures that all the changes that need to be made are made -- but it is a fundamental problem with all low level language. They all suffer from low abstraction, i.e. a certain interface can represent a smaller number of implementations than in high-level languages (even if the choice is not explicit in the type, like, say, in C, the usage pattern is part of the interface). But Rust's choice to expose such details in the types has its downsides as well. > If you use C, you can use formal methods to prove the absence of undefined behaviors C now also has sound static analysis tools [2] that guarantee no undefined behaviour with a nearly fully automatic proof that scales to virtually any code size and requires relatively little effort, certainly compared to a rewrite. [1]: Another low-level language with an emphasis on the same goal of correctness, Zig, takes an approach that is radically different from Rust's and is so simple it can be fully learned in a day or two. Which of the two approaches, if any, is better for correctness can only be answered empirically. [2]: Like https://trust-in-soft.com/ https://trust-in-soft.com/, from the makers of Frama-C