4 ms·
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 th
by tel 12y ago
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 http://r6.ca/blog/20120708T122219Z.html
- marvy 12y agoWow, that link is really something. I never would have thought that someone would release code into the wild without ever running it.
- AnimalMuppet 12y agoDonald Knuth, IIRC, once said, "Be cautious running the following code; I have only proven it correct, not tested it."
- dllthomas 12y ago"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 http://www-cs-faculty.stanford.edu/~uno/faq.html
- dllthomas 12y agoThe 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.
- Jtsummers 12y agoIt 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."
- dllthomas 12y agoI 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...
- tel 12y agoYou 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.)
- marcosdumay 12y agoFrom 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.
- HCIdivision17 12y agoHuh, 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.
- dllthomas 12y agoIt seems entirely reasonable to me to view dimensional analysis as a type system itself.
- tel 12y agoIt 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.