Formal Verification: The Gap Between Perfect Code and Reality https://raywang.tech/2017/12/20/Formal-Verification:-The-Gap-between-Perfect-Code-and-Reality/
Good critique of how formal verification techniques can be extremely heavyweight. Also discusses (rather pessimistically) how it's important to know which parts are not verified
miniblog.
Related Posts
Structs are great in Rust, but sometimes I find them a bit heavyweight. There's a little more syntax than e.g. OCaml, for type definitions and usages.
I end up using more structs (records) in OCaml as a result.
rust-analyzer has "convert tuple to named struct", which helps.
I rather like the fs.readFileSync API in node. It gives you a buffer, unless you specify a text encoding.
This gently encourages users to think about their encoding, without having a heavyweight unicode datatype.
