We take a look at `functional correctness` using refinement types and `flux `- a refinement-type checker for Rust.
- introduction to functional correctness
- use-cases:
- memory mapped IO,
- control-flow with bounds-checking,
- developing parsers
- etc.
- flux - a refinement type checker for Rust
- examples
0:00:00 context for the stream
00:06:13 intro to refined types, functional correctness, use-cases
00:24:00 flux - refining types in rust
00:27:50 using flux, examples
00:48:48 flux playground, more examples
00:52:11 more on formal methods, constraint solvers
01:00:36 Q & A
Links : https://levelup.gitconnected.com/preserving-the-programmers-intent-in-unsafe-rust-beaa3266f43f
#programming #functionalsafety #rust #embeddedsystems