This is precisely what I said in the next paragraph and even mentioned away to correctly encode that "correctness". Where a _correct_ implementation of reverse

This is precisely what I said in the next paragraph and even mentioned away to correctly encode that "correctness". Where a _correct_ implementation of reverse has the property `strHead' s = strTail' (reverse s)` recursively. It's important to understand that type systems can encode correctness to the level you can specify it. So the program is therefore bug-free to the accuracy of your requirements on it. Most people do not work with type systems which can do this and are unfamiliar with formal verification. The author presents directly (and argues through out) that there is a correlation not that bug free and static analysis are the same thing.