4 ms·
F* primary aim is correctness - think something between Coq/LEAN/Isabelle and OCaml/F#. It uses a dependent type system to verify deep functional properties of
by mmoskal 6y ago
F* primary aim is correctness - think something between Coq/LEAN/Isabelle and OCaml/F#. It uses a dependent type system to verify deep functional properties of programs (say that qsort actually sorts, or that a tree is balanced and implements a mathematical map).
Typically such languages are more academic than F*.
- wolfspider 6y agoI would also say take a look at Bosque it is also from the same camp as F* but much simpler to use Z3 with.