# Stacked Borrows talk @ POPL2020 **URL:** \ **Category:** language design\ **Created:** [February 11, 2020, 8:41am UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780 "2020-02-11T08:41:05Z")\ **Posts on this page:** 10\ **Page:** 1
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [February 11, 2020, 8:41am UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/1 "2020-02-11T08:41:05Z")
The recording of my Stacked Borrows talk is available online now: [https://www.youtube.com/watch?v=h9Fh4jRDGLo](https://www.youtube.com/watch?v=h9Fh4jRDGLo) If you want to know more about this work, see [https://plv.mpi-sws.org/rustbelt/stacked-borrows/](https://plv.mpi-sws.org/rustbelt/stacked-borrows/) and [https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md](https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md). ---
**Author:** ![mark-i-m](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/mark-i-m/32/3167_2.png) [@mark-i-m](https://internals.rust-lang.org/u/mark-i-m)\ **Post date:** [February 13, 2020, 1:38am UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/2 "2020-02-13T01:38:42Z")
The talk is excellent btw. Very approachable. ---
**Author:** ![PoignardAzur](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/poignardazur/32/6464_2.png) [@PoignardAzur](https://internals.rust-lang.org/u/PoignardAzur)\ **Post date:** [February 13, 2020, 9:09am UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/3 "2020-02-13T09:09:15Z")
So how "production-ready" is Rustbelt, exactly? Is it mature enough to justify use of Rust in safety-critical systems? I ask because I'm working in a sector with a lot of safety-critical software (nuclear power) and I'd be interested to know if I can point my bosses towards Rust yet. ---
**Author:** ![CAD97](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/cad97/32/3460_2.png) [@CAD97](https://internals.rust-lang.org/u/CAD97)\ **Post date:** [February 13, 2020, 11:58pm UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/4 "2020-02-13T23:58:40Z")
For safety-critical usage, you probably need something like [Sealed Rust](https://ferrous-systems.com/blog/sealed-rust-the-plan/). As I understand it so far, RustBelt primarily focuses on verifying the semantics of Rust and the soundness of the "scoped unsafety" principle (as well as parts of the standard library), but Sealed Rust would be a subset of Rust actually certified to do exactly what it should be doing. ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [February 14, 2020, 8:54pm UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/5 "2020-02-14T20:54:40Z")
My knowledge of safety-critical systems and their certification is very limited, but RustBelt is certainly not aimed at anything that has to do with convincing certification authorities. 😉 Indeed "Sealed Rust" looks to be much more up that alley. Its goals are fairly orthogonal to RustBelt -- at least to my knowledge, certification of safety-critical systems does not usually entail a full formal verification in a proof assistant. We have proofs that give us the utmost confidence that _our model of Rust_ and these data structures are sound. But for safety-critical applications, we have not done nearly enough work to make sure that the model matches the reality. Conversely, I expect Sealed Rust to spend a lot of effort on things like testing the compiler to match some spec, and less on verifying formally that `RefCell` cannot possibly cause UB in safe code no matter the code. (Also did I mention that the thought of having to do anything with the software that runs a nuclear power plant is really, really scary?^^) ---
**Author:** ![PoignardAzur](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/poignardazur/32/6464_2.png) [@PoignardAzur](https://internals.rust-lang.org/u/PoignardAzur)\ **Post date:** [February 16, 2020, 2:40pm UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/6 "2020-02-16T14:40:05Z")
> [@RalfJung](#): > > My knowledge of safety-critical systems and their certification is very limited, but RustBelt is certainly not aimed at anything that has to do with convincing certification authorities. 😉 So, dumb question, but what is it for? > [@RalfJung](#): > > (Also did I mention that the thought of having to do anything with the software that runs a nuclear power plant is really, really scary?^^) Fun fact: nuclear power control systems don't actually run software, in the "lines of code" sense. They are actually controlled by "hand-made" electronic circuits, that are drawn by engineers using specialized software for circuit-drawing, and then go through like a billion layers of verification. (at least that's how Framatome does it) These circuits are either built as-is, or compiled and emulated on a CPU or FPGA or some other kind of specialized chips, depending on the plant. Most countries require at least two different types of architecture to avoid any possibility of common-cause failure; Britain in particular requires that at least one layer of redundancy be a physical, non-emulated electronic circuit. ---
**Author:** ![PoignardAzur](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/poignardazur/32/6464_2.png) [@PoignardAzur](https://internals.rust-lang.org/u/PoignardAzur)\ **Post date:** [February 16, 2020, 2:42pm UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/7 "2020-02-16T14:42:02Z")
Looking at their blog posts, it sounds like we're gonna have to wait a few more years before it can be sold to managers in safety-critical domains who have no prior knowledge of Rust. ---
**Author:** ![Tom-Phinney](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/tom-phinney/32/3299_2.png) [@Tom-Phinney](https://internals.rust-lang.org/u/Tom-Phinney)\ **Post date:** [February 16, 2020, 3:17pm UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/8 "2020-02-16T15:17:34Z")
Disclaimer: I've been retired from this field for a few years, so don't know current common practice (and never did know **worst** practice, as that is always a closely-held supplier secret, at least until public post-upset event analysis 😭). During my era safety shutdown systems for reactors were always implemented in relatively-transparent hardware using redundant sensors, actuators and logic. Common-mode failure analysis was used to avoid obvious shared failure mechanisms. Nevertheless the designers were human, so some unanticipated common-mode failures were not caught (e.g., the failures present in Three Mile Island and Chernobyl, which were in part due to human operator actions). Rust, like Ada, is an obvious long-term candidate base language for safety-critical software. However it's virtually certain that a constrained safety-critical subset language will be required, similar to Ada [SPARK](https://en.wikipedia.org/wiki/SPARK_(programming_language)). That subset likely will employ [design-by-contract (DBC)](https://en.wikipedia.org/wiki/Design_by_contract) and formal verification tools, similar to SPARK. **Addendum to bring this post on-topic** : RustBelt and Stacked Borrows provide some of the theoretical underpinnings for the safety analysis of Rust and its libraries (e.g., `core`, `libc`). Of themselves they are insufficient to demonstrate the safety of Rust code, which demonstration inherently must reflect the intended purpose of the code. ---
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [February 16, 2020, 4:19pm UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/9 "2020-02-16T16:19:14Z")
> [@PoignardAzur](#): > > So, dumb question, but what is it for? It's about making sure that Rust-style borrowing with lifetimes actually works (i.e., that it excludes all memory and thread safety issues), and that APIs like `Rc`, `Mutex` or `RefCell` are actually safe to use by any possible well-typed client (i.e., that the unsafe code in there is properly encapsulated -- and that encapsulation again relies a lot on lifetimes). This is validating some of the core _concepts_ of (idealized) Rust, in an iron-clad machine-checked mathematical proof. We did not have the primary goal of ensuring that the _implementation_ of these concepts is correct. Formally verifying rustc and its LLVM backend would be... rather impossible, I'd say, except if some billionaire shows up and wants to fund it. 😉 ---
**Author:** ![system](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/system/32/14092_2.png) [@system](https://internals.rust-lang.org/u/system)\ **Post date:** [May 16, 2020, 4:19pm UTC](https://internals.rust-lang.org/t/stacked-borrows-talk-popl2020/11780/10 "2020-05-16T16:19:23Z")
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.