Everything you write is true, and the people you cite are quite correct. I used to say
Types are obstructions in the maze of programming: too many of them,and there’s no way thru; too few, and there are too many dead-ends; just enough, and there’s exactly one path – to the exit.
But I didn’t mean that. For critical algorithms and protocols, modeling will never be enough: it requires proof. And for that, as I noted, Hoare-logic-style proofs seem more… effective than the constructive logic I ingested like mother’s milk, back in my academic career.
I recognize that a book like Gries’ is pretty formidable. But I would suggest that working thru all the homework problems in it would be valuable. It really is different than modeling, different than picking the right types. And I say this, as a rabid, rabid Ocaml bigot who really does believe the maxim I wrote above.
ETA: Upon re-reading, it occured to me that I didn’t give an example. So here’s one: suppose you want write a general topological-sort package for graphs, which deals with cycles, and also is able to support a programmer-specified comparison-function on nodes, so that nodes that aren’t related by the partial order are enumerated by the sort in an order consistent with the comparison function.
[An example of why that might be useful is if you’re sorting function-definitions that were written without regard to which ones reference which other ones (no “define-before-use”) and obviously if function A doesn’t mention function B (nor by any transitive chain of mentions) then you’d like these two functions to come out in the same order they went in. So you might use ( * ) as the “node-name”.]
Anyway, it’s not completely straightforward to get this right, and in the process actually -proving- that the code works as desired is useful. And I don’t quite see how better types can help with that burden.