This is an automated archive made by the Lemmit Bot.

The original was posted on /r/programminglanguages by /u/DreadY2K on 2024-09-14 17:18:12+00:00.

At my day job, I write a bunch of code in Rust, because it makes memory safety a lot easier than C or C++. However, Rust still has unsafe blocks that rely on the programmer ensuring that no undefined behavior can occur, so while writing code that causes UB is harder to do on accident, it’s still possible (and we’ve done it).

I’ve also lately been reading a bunch of posts by people complaining about how compilers took UB too far in pursuit of optimizations.

This got me thinking about formal verification, and wondering if there’s a way to use that to make a systems-level language that gives you all the performance of C/C++/Rust and access to low-level semantics (including pointers), but with pointer operations requiring a proof of correctness. Does anyone know of such a language/is anyone working on that language? It seems like it’d be a useful language to have, but also it would have to be very complex to understand the full breadth of what people do with pointers.