I've been exploring ways to reason about some of my embedded-rust implementations and came across a few useful (and really helpful) techniques.
From what I have learnt (as on date), Rust has 3 usable options here (the last 2 are a sort of limited but focused set of formal methods techniques) -
-
type enriched or type-driven programming - we can do a limited form of refinement typing with
const_generics
here but this is definitely something to look forward to, in this space. - property based testing - Crux-mir is simply an awesome tool. It takes a while to set-up but once you get it working, we can get quite creative with our testing.
- automated reasoning tools - We still don't have full fledged support for specifying pre +post conditions or invariants in unsafe Rust but we're getting there with Prusti for safe rust and haybale, which enables us to reason about code.
Here's a tiny post on this for comments or thoughts: