Author: Stephan Sokolow
Created at: 2025-11-19 08:50
Number: 133
Clean content: dimaqq: To recap, every proof is against a certain fixed set of assumptions. Meanwhile what happens in practice is that software is reused in ways unpredictable a priori. RustBelt has proven something about Rust, but not about Rust use in CPython, or Rust use in 3rd party Python extensions and certainly not about Rust used within CPython when an arbitrary user program is run by the interpreter, with arbitrary additional extension, for arbitrary goals and with arbitrary thread model. While I agree that focus should be on other benefits (eg. I spent a decade in /r/rust/ and people coming from C++ loved the tooling most), I think it goes too far to call “proven safe” smoke and mirrors. That stance generalizes far too easily to things like “It’s a waste of time to make Python memory safe because import ctypes exists”, which makes it far too easy for people to dismiss… especially when the whole point of things like the safe/unsafe split and the way parts of Rust have been formally verified is to draw boxes around bits of code and say “assuming no external factor, such as bad RAM or abuse of unsafe violates the invariants, this code’s behaviour will meet expectations”.
