If you're hoping to catch a specification error, don't use a type like `Integer -> Integer`, which doesn't capture the specification except in a most general sense.
Just as you should write good tests, that actually test for useful properties, so you should write good types -- and get useful proofs back from the compiler as a result.
I wasn't trying to catch the error of "program author is a moron who doesn't know the difference between Fibonacci and factorial". Were I trying to catch that error I would have been aware of it, and then much less likely to write the bug in the first place. This is a truism that is well accepted by testing proponents: which tests you write are incredibly important, and you need to write your tests first in order to avoid a curve fitting problem (so to speak). Any non-trivial test would have shown my function to be very broken, what type would you have used to represent that so it wouldn't compile?
Numerical algorithms suffer from a paucity of types. So either you enrich your numerical type hierarchy, or you prove an implementation matches a model, e.g. for fibonacci http://stackoverflow.com/a/8434107/83805
I don't have a response to that, other than to say, now you know why I decided to write compilers instead of pursue a graduate degree in computer science.
The point about a static type system not catching all errors is well taken[1], but if a programmer has mixed up factorial and Fibonacci I would expect that their tests would reflect this as well as their code. This is more the sort of thing you should rely on code reviews to spot.
[1] Isn't the old joke in Haskell "If your program compiles it probably does something someone would find useful, but not necessarily the useful thing you want"
It's not unreasonable, it only seems unreasonable because of the context. I've seen several really good programmers (and overall bright people) mix the implementation of the two up.
