4 ms·
> those applications need the proof for correctness so that more dangerous code---say, what would need `unsafe` in Rust---can be safely added There are actuall
by bennettnate5 3y ago
> those applications need the proof for correctness so that more dangerous code---say, what would need `unsafe` in Rust---can be safely added
There are actually already tools built for this very purpose in Rust (see Kani [1] for instance).
Formal verification has a serious scaling problem, so forming programs in such a way that there are a few performance-critical areas that use unsafe routines seems like the best route. I feel like Rust leans into this paradigm with `unsafe` blocks.
[1] - https://github.com/model-checking/kani https://github.com/model-checking/kani
- lifthrasiir 3y agoYeah, I'm aware of Kani, but it is not optimal for many reasons, including but not limited: hard to install in some cases, loop unrolling is mandatory and does not scale in general (this is a main issue with bounded model checkers, not just Kani), and hard to give hints for efficient verification and/or harness generation. And Kani makes use of CMBC, which is a model checker for C/C++, so Rust is not even special in this regard.