>You’d have to write virtually all the same tests in this type of use case whether you are using the static typing approach or not. No, I don't need to write t

>You’d have to write virtually all the same tests in this type of use case whether you are using the static typing approach or not. No, I don't need to write tests, it I could prove something with types. Here is an example of quicksort, where all invariants and properties are ensured with types, so this code does not need any tests at all. https://github.com/FStarLang/FStar/blob/master/examples/algorithms/QuickSort.Array.fst https://github.com/FStarLang/FStar/blob/master/examples/algo... >integration tests You could reason about your program's correctness on any level with types.