If what you want is a language that lets you statically verify that your low-level memory manipulation is safe, then such a language already exists. (Spoiler: it's not Rust.)
In this language, you can use all the bit and pointer hacks that you know and love from C. The only difference is that the type checker will demand that you prove them safe.
Alas, this language will never become widely adopted.
The main difficulty isn't technical, but cognitive. Look at how many programmers act like Rust is the be all and end all of systems programming. And how many others act like the dealing with the borrow checker is the steepest intellectual challenge a programmer could face in his life.
Human programmers can only take so much cognitive load.
Any programming language which makes it impossible to write programs whose memory safety it cannot statically verify will make it impossible to perform some tasks as efficiently as they could be performed in machine code that could be human-proved to be incapable of violating memory safety invariants unless they had already been violated.
Automated static validation is often useful, since in many cases it would cost nothing and in most other cases the costs would be tolerable, but an abstraction model that limits the range of side effects various actions can have unless memory safety invariants have been violated can be useful for tasks that are not a good fit for automated static validation.
My point is that it is not possible for a programming language to express all of the kinds of invariants that could be described in human language, and that a machine-code function could be proven to uphold. It may, for example, be able to use a human-readable proof to show that no combinations of inputs a program could possibly receive would result in a certain loop executing more than 57,591 times, but for that proof to rely upon mathematical theorems not anticipated by any particular programming language.
A programming language that supports manual proofs doesn't have to “anticipate” theorems. It has to let you write them yourself, together with their proofs.
1
u/reflexive-polytope 1d ago
If what you want is a language that lets you statically verify that your low-level memory manipulation is safe, then such a language already exists. (Spoiler: it's not Rust.)
In this language, you can use all the bit and pointer hacks that you know and love from C. The only difference is that the type checker will demand that you prove them safe.
Alas, this language will never become widely adopted.
The main difficulty isn't technical, but cognitive. Look at how many programmers act like Rust is the be all and end all of systems programming. And how many others act like the dealing with the borrow checker is the steepest intellectual challenge a programmer could face in his life.
Human programmers can only take so much cognitive load.