Hacker News Reader

Comment by kingkilr | Hacker News Reader

    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/ is a totally correct program.

View on HN

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.

If you write compilers, it would be really beneficial if you had a curiosity about the state of the art in programming languages.

… And lo, PHP-2 was born into the world.

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"

Very elegant way to show a point...

He qualified with "reasonably convinced", and you countered with an unreasonable example. That is the definition of attacking a strawman.

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.

If you have the two algorithms mixed up, unit tests aren't going to save you either. Nothing will ever save you from intending to do the wrong thing.

If you actually use the result of the function somewhere, some tests of that component should give wrong answers.

I 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.

Reply on news.ycombinator.com