← Back to context

Comment by nextaccountic

10 days ago

> It's fascinating that this kind of bug is exactly you can't really avoid even when rust is supposedly to guard against.

Note that Rust is not a theorem prover and Rust programs are usually not formally verified (there are some extensions like Creusot to verify Rust programs, but they are incomplete and a work in progress)

Compiler bugs are, like, just logic bugs. There's a project to eliminate compiler bugs that cause unsoundness, project zero [0] but, still, without formally verifying the implementation, there is nothing really guaranteeing there's no such bugs left.

(note: unsoundness in this context means having safe code cause UB due to a compiler bug; the fix is usually to make the compiler reject the code with a compiler error)

To make matters worse, Rust still doesn't have a spec, and there is not even a tight definition of what are the rules of unsafe code - that is, what rules you must follow so that you unsafe code doesn't trigger UB. Discussions around this are done mainly in issues of the unsafe code guidelines repo [1]

[0] https://goals.rust-lang.org/2026/roadmap-project-zero.html

https://github.com/rust-lang/unsafe-code-guidelines/issues

> Note that Rust is not a theorem prover

Not that that would make any difference, theorem provers can also have bugs. Famously this summer someone “disproved” the collatz conjecture by exploiting a soundness bug in Lean.