I've been thinking for some time that one of the key advantages of Rust's safe/unsafe code will turn out to be that formal methods can be applied to the unsafe parts.
Safe Rust is truly safe if it only calls safe Rust or if all the unsafe code is correct.
And safe Rust is a little too inflexible to do certain things, so the unsafe word is a necessary evil. But turns out it's not a bug, it's a feature because now you can trivially identify which parts of the codebase require extra scrutiny to avoid memory corruption and data races.
With FM the main downside has always been the added cost and development time/complexity, needing to use obscure academically oriented systems that most developers have no experience with, etc. But that complexity is probably okay for a project like the Rust standard library, which is already a highly complex project and will only be majorly worked on by a relatively small subset of Rust developers. So you could save some of that cost by only needing it in a (relatively) small part of the ecosystem.
Ofc I realise this wouldn't give the same level of correctness as doing all code with FM. You could only verify whatever guarantees Rust provides for code with no unsafe codepaths. And proofs can have bugs too. But still I think it could increase safety a lot.
The Rust standard library is quite big, not compared to Python obviously, but compared to the scale of things we'd usually apply formal methods to.
It also relies heavily on stuff that's not Rust. For example it's one line in Rust to decide to suppose this whole file named "C:\myfile\stuff.txt" is UTF-8 text, so put it all into a String - the standard library reflects the obvious ways that could fail, maybe there is no such file, maybe it's actually a JPEG and not UTF-8 text, maybe the file is so enormous it can't be represented in RAM on this (presumably 32-bit) computer - but it's relying on the operating system to actually have a working filesystem, you can't use formal methods to deal with such things.
Unlike std, core is mostly stuff the language itself assumes exists. Rust's fundamental types all have methods for example (e.g. 'x'.is_ascii() is true) unlike say C, and the implementation of (most of) those methods lives in core.
Well, core is clearly the place to start, otherwise anything above it in the lib hierarchy would be on non-verified ground anyway. I think it would then be worthwhile to at least start on the alloc crate. A lot of the datastructures use quite a few unsafe concepts for optimisation and getting around the borrow-checker without having to resort to runtime checking. Formally verifying Vec, Hashmap and friends would obviously pay huge dividends across the entire rust ecosystem in terms of overall safety, and should be perfectly surmountable(at least modulo the behaviour of OS memory management). And there's no reason you couldn't do it module by module.
I doubt it. Formal verification helps you prove your algorithms are correct. Bugs from unsafe rust are going to be way more subtle than that, like accidentally assigning a string and crashing [1].
Comments
I've been thinking for some time that one of the key advantages of Rust's safe/unsafe code will turn out to be that formal methods can be applied to the unsafe parts.
Safe Rust is truly safe if it only calls safe Rust or if all the unsafe code is correct.
And safe Rust is a little too inflexible to do certain things, so the unsafe word is a necessary evil. But turns out it's not a bug, it's a feature because now you can trivially identify which parts of the codebase require extra scrutiny to avoid memory corruption and data races.
With FM the main downside has always been the added cost and development time/complexity, needing to use obscure academically oriented systems that most developers have no experience with, etc. But that complexity is probably okay for a project like the Rust standard library, which is already a highly complex project and will only be majorly worked on by a relatively small subset of Rust developers. So you could save some of that cost by only needing it in a (relatively) small part of the ecosystem.
Ofc I realise this wouldn't give the same level of correctness as doing all code with FM. You could only verify whatever guarantees Rust provides for code with no unsafe codepaths. And proofs can have bugs too. But still I think it could increase safety a lot.
The Rust standard library is quite big, not compared to Python obviously, but compared to the scale of things we'd usually apply formal methods to.
It also relies heavily on stuff that's not Rust. For example it's one line in Rust to decide to suppose this whole file named "C:\myfile\stuff.txt" is UTF-8 text, so put it all into a String - the standard library reflects the obvious ways that could fail, maybe there is no such file, maybe it's actually a JPEG and not UTF-8 text, maybe the file is so enormous it can't be represented in RAM on this (presumably 32-bit) computer - but it's relying on the operating system to actually have a working filesystem, you can't use formal methods to deal with such things.
It could make more sense to do the same to Rust's core library: https://doc.rust-lang.org/core/
Unlike std, core is mostly stuff the language itself assumes exists. Rust's fundamental types all have methods for example (e.g. 'x'.is_ascii() is true) unlike say C, and the implementation of (most of) those methods lives in core.
Well, core is clearly the place to start, otherwise anything above it in the lib hierarchy would be on non-verified ground anyway. I think it would then be worthwhile to at least start on the alloc crate. A lot of the datastructures use quite a few unsafe concepts for optimisation and getting around the borrow-checker without having to resort to runtime checking. Formally verifying Vec, Hashmap and friends would obviously pay huge dividends across the entire rust ecosystem in terms of overall safety, and should be perfectly surmountable(at least modulo the behaviour of OS memory management). And there's no reason you couldn't do it module by module.
I doubt it. Formal verification helps you prove your algorithms are correct. Bugs from unsafe rust are going to be way more subtle than that, like accidentally assigning a string and crashing [1].
[1] https://lucumr.pocoo.org/2022/1/30/unsafe-rust/