28 ms·
I'm going to make a few comment and nitpicks. "Patronising those outside the faith ... Please drop the condescending tone." This is a great sentiment, but ra
by tome 12y ago
I'm going to make a few comment and nitpicks.
"Patronising those outside the faith ... Please drop the condescending tone."
This is a great sentiment, but rather jarring to have it followed up by "No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments".
"Equivocating around “type-safety”"
Surely it's reasonable to use the terminology "type safety" to describe a range of properties that code may have beyond the (supposed) original meaning of "memory safety".
"If everyone would just use a modern language with a fancy type system, all our correctness problems would be over, right? ... Type systems cannot be a one-stop solution for specification and verification."
This is an enormous straw man. No fan of strongly typed languages claims that they solve all correctness problems. Furthermore, the fans of strongly typed programming are the most likely to appreciate the additional forms of verification that Stephen outlines.
- AnimalMuppet 12y ago> This is an enormous straw man. No fan of strongly typed languages claims that they solve all correctness problems. I have read the claim "If it compiles, it works" (or minor wording variations), on this board, more than once (in reference to Haskell). Fans of strongly typed languages do in fact make claims that sure sound like they are saying that.
- tel 12y agoIt'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.)
- coolsunglasses 12y agoPeople get excited when they find out they can have types that are expressive, eliminate many useless bad programs almost for free, and be working in a language more expressive than most.
- lelandbatey 12y agoI don't think "people get excited when they encounter convenient sets of features" is a reasonable excuse for misleading claims like "if it compiles it works." It is a reasonable explanation for why some people make these claims (over excitement), but they still shouldn't be misleading people like that.
- coolsunglasses 12y agoHere I point you to what tome & tel said. If it's so clearly nuts, why are you picking that interpretation? Do you read everyone's words in the least-charitable/sensible light possible?
- AnimalMuppet 12y agoI can't speak for lelandbatey. For myself, though, I picked that interpretation because that really seemed to be what they were trying to say. I'm not looking to take peoples' words in the least-charitable way possible, but I'm also not going to go out of my way to make excuses for them when they say something that is clearly wrong.
- coolsunglasses 12y agoI cannot say that getting upset over people using jokey memes to communicate ideas (Haskell is more likely to be correct after a successful type-check than other langs) is likely to do you much good. I like Epictetus for when I notice I am upset about something that isn't within my control: http://classics.mit.edu/Epictetus/epicench.html http://classics.mit.edu/Epictetus/epicench.html
- tome 12y agoThe claim "If it compiles, it works" taken literally is so trivially falsifiable that it cannot reasonably be interpreted as a serious claim that types "solve all correctness problems". EDIT: I propose that next time you read "If it compiles, it works" you reply with "Are you suggesting that types solve all correctness problems?" I guarantee you that you will not get an affirmative response. EDIT: I do however take the point that fans of strongly typed programming should act to moderate the excitement of some amongst their numbers in order to reduce the incidence of ambigous or misleading claims.
- seanmcdirmid 12y agoI've always taken it as meaning, "If it compiles, it must works, otherwise you're in trouble;" given that debuggers for Haskell are still relatively immature (especially for its age), your best bet is to lean heavily on the type system.
- eru 12y agoYou can still run tests. Debuggers are great for figuring out why your program is wrong and how to fix it. But they seldom alert you to problems in the first place. Tests do.
- seanmcdirmid 12y agoUndoubtedly--tests, static types, debugging--I want them all!
- sanxiyn 12y agoThis is a Haskell-specific problem. OCaml has an excellent debugger, not to speak of F#.
- seanmcdirmid 12y agoOCaml and F# are also more conventional. Lazy evaluation is a pain during debugging; even using laziness in a language like C# can be troublesome when you hit the debugger. So if you are going to rely on a lot of it, might as well have a lot of static typing to avoid debugging it.
- fsloth 12y agoIf the program is a composed from trivial data conversion steps that are implementable using standard transforms (C++:s stl algorithms, ML:s folds, etc) then it is very likely that it works when it compiles. If there are various branches in the logic and I can encode those branches using types as invariants then that eliminates a particular category of bugs altogether which reduces logical errors. If I use immutable variables it helps even more. I'd say the 'compiles and works' means that if one can leverage existing operations on containers and use types as helpfull invariants then those two stylistic choices reduce the possible number of bugs in various categories. I would not claim all errors are removed... e.g. numeric code that depends on the precision of arithmetic on floating points is as error prone with or without static types.
- mercurial 12y agoI can confirm that "If it compiles, it works" is tongue in cheek. However, it's also true that I feel confident that a program in OCaml will be working correctly either the first time, or shortly afterwards, once it compiles (and, just as importantly, will keep working tomorrow or break at compile time). Knowing that the compiler eliminates for you a large amount of potential mistakes is a huge relief, and lets you focus on the parts of your program where the compiler cannot help you and where logic errors are lurking - especially where you are manipulating several values of the same type.
- eli_gottlieb 12y agoMost of the time, that's tongue-in-cheek. On the other hand, when working with dependent types, the specification is a type, and if the theorem giving that specification type-checks (ie: the "proof" is a program of the appropriate type), then the code is correct, period. Of course, attempting to prove the theorem can be hair-pullingly frustrating and takes valuable time, but it will expose the assumptions and corner-case you weren't thinking clearly about.