5 ms·
I'm reasonably convinced that once my program has passed the typechecker, it is logically correct Yup, this is one of my favorite things about Haskell, that's
by kingkilr 14y ago
I'm reasonably convinced that once my program has passed the typechecker, it is logically correct
Yup, this is one of my favorite things about Haskell, that's how I know that http://bpaste.net/show/32033/ http://bpaste.net/show/32033/ is a totally correct program.
- dons 14y agoIf 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.
- kingkilr 14y agoI 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?
- dons 14y agoNumerical 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 http://stackoverflow.com/a/8434107/83805
- kingkilr 14y agoI 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.
- swah 14y agoVery elegant way to show a point...
- Symmetry 14y agoThe 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"
- drunkpotato 14y agoHe qualified with "reasonably convinced", and you countered with an unreasonable example. That is the definition of attacking a strawman.
- kingkilr 14y agoIt'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.
- deleted 14y ago[deleted]
- afrozenator 14y agoI forget whose quote this is - The computer is a wonderful machine, it does what I tell it to do, not what I want it to do. Your point taken, but that is a problem in programming language X, which has Y type system, for all permissible values of X and Y.