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