Re:Functional Algorithms, Verified
by namibj on Saturday October 16, 2021 @03:11AM
(#28886139)
1) For the "how to get started with formal verification outside academia", I'll first get the case of "in/for production" out of the way:
a) "use Z3[0] with some binary/source-language-of-choice/LLVM -lifting to handle relatively simple situations that need to":
i) guarantee some assert (often, but not always index-out-of-bounds checks, like non-trivial Rust slice indexing) statements are unreachable
ii) some bit hacks compute the same thing as the non-hacked implementation
b) "use TLA+[1] to verify concurrent stuff with race conditions":
i) in lock-free data structures that don't come with a proof that the algorithms do the right thing (in those cases, just verify three implementation truly matches the proven algorithm)
ii) in (network, or sufficiently network-like) protocols that aren't 100% exactly transcribed ports of existing proven algorithms or so simple a finite state machine can (and will) be used
2) For doing it more for fun than short-term gains:
a) For getting a handle on pure functional program design, I recommend going through the relevant track of HtdP[2] (Prologue until just before "Arithmetic and Arithmetic" -> I -> II -> III -> Intermezzo 2: Quote, Unquote -> V {-> [if you want to write remotely-performant pure functional code, follow up with:] VI})
b) For learning how to exploit a proof assistant for fun and applied computer science, I'll refer to the guidance provided by Isabelle/HOL.
Please use the IRC(/Matrix ?)[3] if you are confused on how exactly to best approach Isabelle/HOL in your case.
a) "use Z3[0] with some binary/source-language-of-choice/LLVM -lifting to handle relatively simple situations that need to": i) guarantee some assert (often, but not always index-out-of-bounds checks, like non-trivial Rust slice indexing) statements are unreachable ii) some bit hacks compute the same thing as the non-hacked implementation
b) "use TLA+[1] to verify concurrent stuff with race conditions": i) in lock-free data structures that don't come with a proof that the algorithms do the right thing (in those cases, just verify three implementation truly matches the proven algorithm) ii) in (network, or sufficiently network-like) protocols that aren't 100% exactly transcribed ports of existing proven algorithms or so simple a finite state machine can (and will) be used
2) For doing it more for fun than short-term gains: a) For getting a handle on pure functional program design, I recommend going through the relevant track of HtdP[2] (Prologue until just before "Arithmetic and Arithmetic" -> I -> II -> III -> Intermezzo 2: Quote, Unquote -> V {-> [if you want to write remotely-performant pure functional code, follow up with:] VI}) b) For learning how to exploit a proof assistant for fun and applied computer science, I'll refer to the guidance provided by Isabelle/HOL. Please use the IRC(/Matrix ?)[3] if you are confused on how exactly to best approach Isabelle/HOL in your case.
[0]: https://github.com/Z3Prover/z3 [1]: https://lamport.azurewebsites.net/tla/tla.html [2]: https://htdp.org/2021-5-4/Book/index.html [3]: [edit: apparently it is neither IRC nor Matrix, but rather Zulip:] https://isabelle.zulipchat.com/