Hacker News Reader

Comment by tel | Hacker News Reader

It's said semi-tongue-in-cheek. The original statement was filled with caveats. [0]

Sometimes it's said less tongue-in-cheek. Then it usually has to do with the facts that large refactorings can be handled by merely breaking things and rewiring until types check. This generally does work since types typically guard "wirings".

But taken out of contexts and as the meaning is extended bit by bit it becomes truly ridiculous and nobody would disagree.

So, don't just propagate the rumor. Nobody is claiming miracles. It just sounds like that at around the 8th iteration of the telephone game.

[0]: As far as I'm aware, this is the origin of the idea: http://r6.ca/blog/20120708T122219Z.html

View on HN

The origin is definitely further back. I recall hearing "it takes longer to get it compiling, but when it compiles it works" about OCaml more than a decade ago. When I mentioned this to my father at that point, he remarked that the sentiment goes back further.

It goes back to discussions on Ada as well. I, personally, qualify my advocacy with a probably. As in, "if it compiles, it's probably correct."

I wouldn't be terribly surprised if he'd been thinking of Ada evangelists, though I think there are other candidates too. Unfortunately, I can't ask him to clarify...

You know, that's certainly correct. I feel like roconnor's post comes to mind for me because of it's audacity more than its primality. I'll make a note in my original comment if I can.

(Edit: I can't.)

From your link:

"...I actually had no idea how the function worked. I simply wrote a function that matched the required type."

I guess everybody have done that. But releasing it without testing... I'm just impressed, in both a good and a bad way.

Huh, you know, that sounds just like how dimensional analysis affects people sometimes. I've certainly seen some take a pile of engineering inputs and whack them together until the units work (myself included); it's a shockingly powerful heuristic for linear systems, since you'll typically only be off by some logical scaling factor. Of course, there's a bajillion ways it can deceive, so it's wise to be thorough.

It seems entirely reasonable to me to view dimensional analysis as a type system itself.

It has to do with how abstract and parametric the code was. There may very well be only one valid type-checking program which exists (so long as you do a cursory check against infinite loops and error throwing).

So, it's a gamble---do there exist any other non-trivial programs at this type?

If not, then I know my code written is correct without testing.

If there are, then I'm risking that I found the right one.

This is why Haskellers get so excited about "parametricity". It's the core tool that exacts this property of "there are only a small number of programs which could ever exist at this type" which drives correctness.

Wow, that link is really something. I never would have thought that someone would release code into the wild without ever running it.

Donald Knuth, IIRC, once said, "Be cautious running the following code; I have only proven it correct, not tested it."

"Beware of bugs in the above code. I have only proved it correct, not tried it."

http://www-cs-faculty.stanford.edu/~uno/faq.html

Reply on news.ycombinator.com