18 ms·

Seven deadly sins of talking about “types” (2014)

131 points by dkarapetyan 12y ago

qznc 12y ago
The coda at the end is nice tool in general. Whenever you find yourself in a discussion, where it seems people talk past each other because some words have a fuzzy meaning, try to avoid the word completely. Works good for discussions about "free will", "love", "intelligence", "luck", "conciousness", and apparently "types".
- pseudonom- 12y ago
  http://lesswrong.com/lw/nu/taboo_your_words/ http://lesswrong.com/lw/nu/taboo_your_words/
pekk 12y ago
I found this wonderfully clear and refreshing and I felt hopeful for the future of programming. In the meantime, it's just nice to see that not everyone is a shambling cultist, repeating canned talking points they read on a wiki which affirm to them that their own choice is the very best choice possible.
- davidgrenier 12y ago
  It's fair to say that but it isn't the case that someone can have an worthwhile opinion of something they haven't tried and a lot of people working with say JavaScript or PHP just have never tried a decent ML-style language in anger. I think Stephen is a tiny bit guilty (as we all are) of that which I'll use Kahneman wording's to put: "Nothing is as important as you think it is when you are thinking about it". There's what seems to be an exaggeration that whatever cost a type system has must be high... it isn't even true of dependently typed programming languages. I also think product and sum types can be given a free pass to most complaints and while at it, you can throw in first-class function type as a minimum. And I will grant that you can stay away from ad hoc polymorphism and subtyping.
  - dragonwriter 12y ago
    > It's fair to say that but it isn't the case that someone can have an worthwhile opinion of something they haven't tried I disagree. I don't have to try hitting myself in the head with a hammer to have a reasonable basis to believe it would be a bad idea. There's not much point in having reasoning ability if you can't apply it to develop useful opinions on what is and isn't even worth trying. Obviously, that's not to say that there aren't additional insights possible from direct experience, and that people sometimes apply prejudice rather than sound reasoning to present opinions on things they haven't tried, but its simply silly to say that people cannot have a worthwhile opinion on something they haven't tried.
    - AnimalMuppet 12y ago
      I think you're misunderstanding davidgrenier's comment, specifically the line you quoted. It appears to me that you are actually agreeing with him.
      - dragonwriter 12y ago
        There may be an "is -> isn't" or "can -> can't" issue in the line I quoted, but I don't think so -- the rest of the sentiment in that article seems to be a specific case where the poster believes that someone is making an error of offering an opinion without experience (which I agree is an error), which makes sense (though, I'd obviously argue, represents an overgeneralization from a valid example) if its supporting a generalization that opinions without experience are invalid, but, without some "but" or "on the other hand", etc., doesn't make a lot of sense if the thesis it goes with is that some such opinions are valid. So I don't think I misunderstood it.
  - pekk 12y ago
    I don't have any problem with ML, nor do I favor Javascript or PHP. Maybe you shouldn't make so many assumptions.
hawkice 12y ago
I have always gotten the impression there was a failure of communication when (without lose of generality) Haskell programmers would tell (also, without loss of generality) Python programmers that Python only has one type, 'object', which appears to violate the understanding of the Python programmer thoroughly enough that there isn't really even a conversation about what is meant by the comment. The first point dissolves this conversation (because clearly neither the Haskell nor Python programmers are confused about the execution of actual programs). Notably, it dissolves it in a way where that pesky third issue doesn't pop up (which is perhaps the worst of them all, sans _maybe_ the last).
- hcarvalhoalves 12y ago
  Well, that's an interesting comment. I have almost a decade experience in Python, and having recently picked up Haskell, I clearly see the value of having (or not) a static type system. I have noticed that during all these years I would just "type-check" the various APIs in my mind, or with the aid of the REPL, but it's not as easy when programmers with less experience join the project. I would often have to explain tracebacks about type errors (e.g., tried to call a missing method on `None`, but the programmer didn't expect that API to return `None`). Strong typing avoids errors from propagating, but without static checking only gets you half-way there. I would still use Python (or other dynamic language) to introduce someone to programming - not having to reason about types lowers some barriers - but nowadays I'm not sure it pays off for a project expected to be maintained.
  - crdoconnor 12y ago
    I was always on the fence about static typing because I figured that it automatically led to more verbose code (clearly a significant down side), but after looking at Haskell and F# I'm not so sure that's true for them, even though it definitely is for C++ and Java. I'm still unconvinced that additional testing is required to overcome bugs that a static type checker would catch, though. In my experience all of those "call a missing method on None" issues get caught relatively quickly by a test that you would have to write anyway even if you were using a language with static typing.
zak_mc_kracken 12y ago
> If somebody stays away from typed languages, it doesn't mean they're stupid, or lack education, or are afraid of maths. There are entirely valid practical reasons for staying away. Please drop the condescending tone. Well, ok, let's hear these practical reasons? Otherwise, it's just an empty claim.
- eru 12y ago
  Legacy code (and skillsets) are always a good practical reason.
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 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
    - 12y ago
tel 12y ago
With deference to Dr Kell, I think this is overwrought. He has some good points, points made happily against a particular form of "type cultist" who oversimplifies argument toward making types out to be something magical. They're not, no sane person would think so, but they are a static, syntactic proof system pertaining to the meaning of your programs and there's a lot to be said for such technology. I am happy to quibble exact points made in this rant, but I'm on my phone so for now I'll merely say that there's a large design space of programming languages and a similarly large (perhap today larger) space of type theories. Matching them up to hit all of your tradeoffs is hard, but there have been some great successes and I would happily contend that any professional programmer owes it to themselves to explore this design space "in anger". I'm also happy to generally claim that faster, more complete feedback is better than the opposite. Static systems of all regards are faster than "dynamic" ones, and most of them are more complete. This is where you hear about comparisons of types (especially dependent ones) and tests. It's great stuff to think about and explore. Further, I want to emphasize that SMT solvers are fascinating too and nobody thinks that they're not. The style of proof they provide is more expressive and less certain, though, so the right answer is to know how to combine all of these modes of evidence.
sanderjd 12y ago
> Type checkers are one way to gain assurance about software in advance of running it. Wonderful as they can be, they're not the only one. This is true, but in my experience they are far and away the most common and easily tooled automatic way. Tests may run automatically, but they must be manually written, and static analysis tools are not (yet?) very widespread.
colanderman 12y ago
No, I think a separate type-level language is a good thing, so long as my data-level language remains Turing complete (and thus undecidable). I would much rather be forced by the syntax -- by the construction of the language itself -- into a guaranteed decidable subset, rather than have to reason things out myself and get frustrated when the compiler doesn't agree with me (or when it used to agree with me and doesn't any longer!). Now, there's no reason that the type-level language can't be exactly a subset of the data-level language. I'd just rather not play guess-and-check decidability with the compiler the same way I currently have to play guess-and-check optimizability.
- marvy 12y ago
  I think the author meant that you don't want two separate Turing-complete languages, one for values at runtime, and another for values at compile time.
- eru 12y ago
  There are good arguments for not even getting Turing-completeness in your value-level language. Totality would be a nice goal. See http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html
  - colanderman 12y ago
    Oh I totally agree. Unfortunately for many that's far too radical a notion, despite how unnecessary Turing-completeness is for 99.95% of programs written, and how desirable termination is. First you have to convince the Ruby/Python/JS/Elixir crowd of the frivolity of code mutability.
breckinloggins 12y ago
Things that also get my goat (from a less type theoretic point of view): - Assuming that type checking is the only thing you might want to do with your program at compile time. There are, in fact, arbitrarily many things you might want to do at compile time. Textual preprocessing, expansion macros, type checking, C++ template metaprogramming, etc. are all obvious examples. The fact that most languages bolt all of these things on as one-off features is a sign that something deeper is being missed (perhaps the 3-Lisp[1] idea, for example, or just consider plain ol' Lisp macros). - Assuming that totality, soundness, and lack of side effects are always type checking virtues. Sometimes I'd like a "typechecker" that isn't always guaranteed to terminate. Sometimes I'd like my typechecker to launch some missiles. This is really more about the previous point. - Assuming that type checking is NOT desired at runtime. Sometimes it is. Clojure's core.typed has the property that it is "just code" and can therefore be run at anytime and used for things other than checking that your code is safe to ship. [2] - Assuming that a program that fails type checking shouldn't be run. Maybe it should and the parts of the program that fail type checking should be run inside some monadic context. Maybe we want not only gradual typing, but gradual enforcement. Maybe if we had richer type data, then "failing type checking" wouldn't be binary. Perhaps a program that fails certain type checks has to add runtime support to enable certain features, but if the same program type checked to be about pure memory locations, the runtime would vanish and a "straight to the metal" program would remain. (In other words, maybe what we currently call a language's "runtime" should just be a residue of things that couldn't be checked at compile time, among other things.) - Assuming that types and the type checker should be a fixed feature of the language. Perhaps type checking should be something that is built as a library from language primitives. Take this far enough and you get something like exotypes. [3] Which reminds me... - Assuming that "type" is the only kind of metadata you might like to attach to a symbol, expression, or value. There are many other things I might like to express, and I might like to use the usual machinery of type checking to analyze or work with those things. Clojure's value-level metadata and Common Lisp's property lists are some good examples of generalizing this. - Focusing on manifest typing for verifiability of programs and ignoring the extra information it gives tooling. Visual Studio's IntelliSense and F#'s type providers are examples. At least one person at Microsoft has trouble sleeping at night because he or she is worrying about when the rest of us are going to figure this one out. [4] - Assuming that most programmers want one or the other. The article touched on this, but I wanted to expound a bit. I would like my original prototype to feel like play-doh and my finished product to feel like concrete. Why do I have to do this in two different languages? "Oh I'll prototype it in python and then switch to Haskell when I want it to be safe." What? - In general, assuming that it is the job of the language designer to provide the safety nets, rather than the DSL or API designer. A suitably designed programming language is one that could prevent operation Foo in layer 3 while allowing it in layers 1 and 2. This is one reason why languages like Idris are so complicated. Dependent types HAVE to be complicated because the language designer feels that it is his or her job to make sure the part of your program that runs at compile time terminates and doesn't do anything "bad". Why do we rarely question this assumption? [1] http://lisp-univ-etc.blogspot.com/2012/04/lisp-hackers-pascal-costanza.html http://lisp-univ-etc.blogspot.com/2012/04/lisp-hackers-pasca... [2] https://github.com/clojure/core.typed https://github.com/clojure/core.typed [3] http://dl.acm.org/citation.cfm?id=2594307 http://dl.acm.org/citation.cfm?id=2594307 [4] http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type-providers-in-pictures.aspx http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type...
cbd1984 12y ago
> It's also nothing to do with static checking—“type safety” holds in all “dynamically typed” languages. This. Exactly true, and often forgotten. It's useful here to distinguish between conversions and casts. Conversions use type information to ensure computations remain sensical; the canonical example is a conversion between integers and floating-point values which makes sure you never end up feeding invalid bit patterns into the relevant arithmetic hardware. An example of a cast is taking a bit pattern you had been treating as an integral value and then telling the language it's a floating-point value, and there not being an error at that point. Conversions don't break the type system; they use the type system. Casts throw types away.
- kyllo 12y ago
  Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload.
  - dllthomas 12y ago
    Arguably, there is an intersection of "cast" and "conversion" where casts are valid.
  - cbd1984 12y ago
    > Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload. This is true. A more interesting example might be a program which creates database queries from user input casting input strings to the type "unescaped string", and then converting them to type "escaped string" by performing a string-escaping process on them. (A cast from "unescaped string" to "escaped string", which is done implicitly very often in languages where those types are not machine-checkable, is often disastrous.)
    - kyllo 12y ago
      Right, but I don't think this sort of type "conversion" (e.g. some function with type signature like this in Haskell) escapeQueryString :: ByteString -> Query is really adding or throwing away type information, it's just a function that accepts one type and returns another type. So it's not related to casting, except that it's the opposite of casting. But what that gives you is the ability to compose it with any other function that you define as accepting a `Query` type, and the program will refuse to compile if you ever accidentally try to pass it a ByteString. So it's about enforcing an invariant, in other words.
michaelochurch 12y ago
The hardest objective problem in computer science may be P ?= NP, but the hardest subjective problem is whether it is better to have static vs. dynamic typing in languages. There are extremely intelligent, thoughtful people on both sides... and it's rare in software engineering that there is such an even divide. I'm quite familiar with Haskell, Scala, Clojure, and many other languages... and I still can't conclusively call one better. I prefer static, on a mix of practical grounds, but I realize that it's not a clear victory. Take the concept of data frames from R, also seen in Python's Pandas library, and probably inspired by the APL family's (column-oriented) tables. It's not a complex concept. Yet it's very powerful for interactive data exploration. It's also a bitch to statically type (see: https://github.com/acowley/Frames https://github.com/acowley/Frames). It's more of a leap than lenses (and probably, like lenses, extremely cool once you fully "get" it). If we have to pull out some advanced Haskell extensions to do something basic in interactive data analysis then I consider that worrying. (This is not to say that Frames isn't a great piece of work. Bringing subtyping into a Hindley-Milner derived language and not having everything go to hell is really hard. See: Scala) And remember, this is coming from someone who's pretty invested in the "static" side. Clojure also has a world-class aesthetic sense. Haskell is still using camelCase. OCaml uses under_scores; that's better than fuckingUglyCamelCase, but not ideal. Clojure (and the Lisp family in general) is run by people who realize that aesthetics are really important and that allowing hyphenated-tokens is far better than allowing people who hate their space bars to write "a-1" when they should be writing "a - 1". That's just one example. For another, maps. Clojure has {"five" 5, "ten" 10} but Haskell has fromList [("five", 5), ("ten", 10)]. My point is that (which I prefer Haskell, for its types) Clojure's aesthetic sense is arguably better, and I would say world-class, especially considering that it runs on a butt-ugly platform (JVM) and is still a beautiful language. We need to keep watching that community closely because they're doing some great work in a wide variety of fields, including front-end development (ClojureScript). Type systems don't just make you write annotations; they force you to structure your code around type-checkability. This is inevitable, since type checking is by definition a specific kind of syntactic reasoning. There is some truth around that. Just to get data frames, you need row types which means you have subtyping, and that complicates type checking considerably. Haskell (see Frames) uses multiple "experts only" language extensions to get something that "just works" for casual use but requires advanced knowledge to grok the types. It's great work, but its difficulty shows that we can't just ignore subtyping. The counter-argument that I'd make is that 95+ percent (maybe more?) of all functions that are ever written ought to have simple static types. So much of code, when it is clean, is already well-typed, even in a dynlang. The difference is that, in a static language, the compiler yells any time someone fucks that up in refactoring. And, more generally, you learn about errors (not all errors, but a surprising percentage of them) sooner and that's a good thing. In a dynamically typed language, you see a lot of functions that evolve into multimethods that do different things per input type(s) and (although usually this won't happen if the code is maintained by decent designers) you can get O(n2) or worse complexity in the functionality. If you're programming defensively in a dynlang, you have to think about all the crap that might be passed into your functions. "What's a Matrix plus a Scalar? How about a RowVector plus a ColumnVector? How about a Sparse2DArray plus a DataFrame?" On the whole, I'd rather be in a statically-typed language for a program of any size, and I'm stodgy and conservative and old (but efficient and concise) so, for me, "big code" starts around a couple thousand lines. I hate writing boilerplate unit tests that a compiler and a type system would knock out automatically. But I do have to give Clojure a lot of props for its community and its aesthetic sense, and I think that the above obviously derive from its ease-of-use and its Lisp heritage, both of which are tied to a feature (dynamic typing) that I otherwise wouldn't much like. The main question that I've been pondering for a few years (and not coming to satisfactory answers) is whether it's possible to unify the cleanness-of-language and aesthetics of Clojure/Lisp with the static typing of Haskell... and not get some hyper-complex type system that results in compile-speed problems at scale (e.g. Scala under typical use). It's an open problem.
eru 12y ago
> (It should also do so using a straightforward explanation, ideally featuring a counterexample or stripped-down unprovable proposition. I don't know any type checker that does this, currently.) I guess the incomplete-pattern-matching warnings (in eg ghc) come closest. They usually give you an example of an example of a value you haven't matched. But that's a very restricted and simple domain.
fsloth 12y ago
I think the argumentation here is a bit a skewed towards 'what static types can and cannot do for the compiler' - i.e. how they can help the computer in constructing formal proofs. For me another almost as valuable thing is how static types help me think about and design the code. The static type information is always there to remind "this entity belongs to this set of objects" which frees me from the cognitive burden of maintaining this constantly in my working memory. With specific static types the function signatures now document the tranforms defined for those entities . This aspect of static types as a cognitive tool is highly personal, and not same for everyone, unlike the language and the compiler, though.
wyager 12y ago
I emphatically reject the many of the conclusions of this article. >Let me say it simply. Type systems cannot be a one-stop solution for specification and verification. Wrong! Any correctness property can be encoded into a sufficiently powerful type system. Which brings me to... >Curry-Howard is an interesting mathematical equivalence, but it does not advance any argument about how to write software effectively. This is absurd, of course. The isomorphism between type systems and proof systems allows us to build lots of impressive systems like Agda and Coq. >No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments. That's actually quite a reasonable desire. >Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code. To the author, this seems to mean "therefore, we shouldn't have types!". In reality, a sufficiently flexible programming language allows you to write type-level code in the same language as value-level code. See Agda. >Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic. Lots of people have typed transducers just fine... http://blog.podsnap.com/ducers2.html http://blog.podsnap.com/ducers2.html http://conscientiousprogrammer.com/blog/2014/08/07/understanding-cloure-transducers-through-types/ http://conscientiousprogrammer.com/blog/2014/08/07/understan...
- djur 12y ago
  > To the author, this seems to mean "therefore, we shouldn't have types!". This doesn't follow from the author's earlier statements about using and benefitting from languages with static type checkers. An ideal typed Lisp dialect would fit the author's requirements.
  - jroesch 12y ago
    An ideally typed Lisp would be no different then a dependently typed language semantically. Yes, you would use slightly different syntax but a key feature of most dependently typed languages is that they only have a single class of pseudo-terms that are used for both types and programs. An example Idris program: double : Nat -> Nat double n = 2 * n ourVectorType : Type ourVectorType = Vect (double 1) Int aVector : ourVectorType aVector = [1, 2] If you change everything above to an S-Exp you have a typed Lisp where both types and terms have the same language.
mercurial 12y ago
> The Sniveley/Laucher talk included a comment that people like dynamic languages because their syntax is terse. Sure. Trying to have a strongly-typed Java program, for instance, means a lot of boilerplate. As a consequence, it's often not done, or at least not done enough. > To suggest that any distaste for types comes from annotation overhead is a way of dismissing it as a superficial issue. On a large codebase, there is nothing superficial about it. The more boilerplate you have, the more difficult it becomes to understand the codebase and to find code which actually does something. > If everyone would just use a modern language with a fancy type system, all our correctness problems would be over, right? If you believe this, you've drunk far too much Kool-Aid. Yet, apparently our profession is full of willing cult members. Let me say it simply. Type systems cannot be a one-stop solution for specification and verification. They are limited by definition. They reason only syntactically, and they specify only at the granularity of expressions. They're still useful, but let's be realistic. Let's be realistic, and not pretend this is a widespread opinion. > Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic. Usually they are captured only overapproximately, which, in turn, yields an inexpressive proof system. The end result is that some manifestly correct code does not type-check. Possibly, but it's all a question of tradeoffs. There is a lot more incorrect than correct code which doesn't typecheck.
- mateuszf 12y ago
  > On a large codebase, there is nothing superficial about it. The more boilerplate you have, the more difficult it becomes to understand the codebase and to find code which actually does something. In case of types it's true for humans. IDE will be able to build a very precise model and ease navigation and code changes when it understands types.
  - superuser2 12y ago
    Why should this be a property of the IDE and not the language itself? No, seriously. If the language sucks but your interaction with the IDE is fine, why not have a language that is closer to your interaction with the IDE to begin with, and use a text editor?
fsloth 12y ago
This topic of "what are static types good for" continued to bug me because I could not formulate a concrete answer to myself. I found the following Reddit discussion http://www.reddit.com/r/programming/comments/lirke/simple_made_easy_by_rich_hickey_video/ http://www.reddit.com/r/programming/comments/lirke/simple_ma... Which had eventually the specific thing I was after in a comment by Rich Hickey which helped to nail the concept I was after "Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system." Which is precisely why I enjoy types: Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism. Which, I think tells exactly what static types are good for: For those sort of problems that benefit from having a formal specification. There are a lot of programs that have this quality. So the argumentation is a bit skewed off. It should not be about whether static or dynamic types are better but more focus on what are those identifiable problem patterns where a dynamic type system helps programmer create more value than a static one and vice versa.
- shadowfox 12y ago
  > Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism. I think this is a valid point. But I am less convinced about the second part. I feel that better type systems do help one model the world better (while retaining the consistency checking that you mentioned). In my mind at least having more/better "type tools" is like having differently shaped pieces in your lego tool box. You can create better models for yourself, because the pieces allow you to. And the more experience you have with them, your modeling abilities also improve.
  - fsloth 12y ago
    The Lego analogy is what I also often like to use :) ! " I feel that better type systems do help one model the world better" I agree. But then again, I prefer to start from scribbling mathematical proof mimicking pseudocode which is easily transferred then to statical types. Some people just bang something together, prototype on the IDE/REPL as they go on and they can probably finish faster than me and produce value. If this figure-this-out-while-coding person then has the craftmanship to clean up the code the result is often as good as with the paper-and-pen-first approach. For larger systems, however, I would claim that starting from careful design pays off more because the code-prototype can quickly get out of hands if there are too many abstractions and variables flying in the air at the same time. The 'formal' approach has pitfalls if applied without taste or experience, since, well, modeling for modelings sake can get out of hands at which point one has a shaking tower of abstraction generated from mental masturbation rather than anything of lasting value. This becomes pathological the minute it reaches production. I think we recognize it all has to do with the experience of the programmer and the dedication but craftmanship is very hard to formalize...
raiph 12y ago
Perl 6 elegantly blends static nominal typing and arbitrarily loose or tight dynamic constraints. The following slides were published a week or so ago and should demolish most folks' overly simplistic view that one or other is best or indeed that they don't play well together: http://jnthn.net/papers/2015-fosdem-static-dynamic.pdf http://jnthn.net/papers/2015-fosdem-static-dynamic.pdf

131 points by dkarapetyan 12y ago

qznc 12y ago

The coda at the end is nice tool in general. Whenever you find yourself in a discussion, where it seems people talk past each other because some words have a fuzzy meaning, try to avoid the word completely. Works good for discussions about "free will", "love", "intelligence", "luck", "conciousness", and apparently "types".

pseudonom- 12y ago
http://lesswrong.com/lw/nu/taboo_your_words/ http://lesswrong.com/lw/nu/taboo_your_words/

pekk 12y ago

I found this wonderfully clear and refreshing and I felt hopeful for the future of programming. In the meantime, it's just nice to see that not everyone is a shambling cultist, repeating canned talking points they read on a wiki which affirm to them that their own choice is the very best choice possible.

davidgrenier 12y ago
It's fair to say that but it isn't the case that someone can have an worthwhile opinion of something they haven't tried and a lot of people working with say JavaScript or PHP just have never tried a decent ML-style language in anger. I think Stephen is a tiny bit guilty (as we all are) of that which I'll use Kahneman wording's to put: "Nothing is as important as you think it is when you are thinking about it". There's what seems to be an exaggeration that whatever cost a type system has must be high... it isn't even true of dependently typed programming languages. I also think product and sum types can be given a free pass to most complaints and while at it, you can throw in first-class function type as a minimum. And I will grant that you can stay away from ad hoc polymorphism and subtyping.
- dragonwriter 12y ago
  > It's fair to say that but it isn't the case that someone can have an worthwhile opinion of something they haven't tried I disagree. I don't have to try hitting myself in the head with a hammer to have a reasonable basis to believe it would be a bad idea. There's not much point in having reasoning ability if you can't apply it to develop useful opinions on what is and isn't even worth trying. Obviously, that's not to say that there aren't additional insights possible from direct experience, and that people sometimes apply prejudice rather than sound reasoning to present opinions on things they haven't tried, but its simply silly to say that people cannot have a worthwhile opinion on something they haven't tried.
  - AnimalMuppet 12y ago
    I think you're misunderstanding davidgrenier's comment, specifically the line you quoted. It appears to me that you are actually agreeing with him.
    - dragonwriter 12y ago
      There may be an "is -> isn't" or "can -> can't" issue in the line I quoted, but I don't think so -- the rest of the sentiment in that article seems to be a specific case where the poster believes that someone is making an error of offering an opinion without experience (which I agree is an error), which makes sense (though, I'd obviously argue, represents an overgeneralization from a valid example) if its supporting a generalization that opinions without experience are invalid, but, without some "but" or "on the other hand", etc., doesn't make a lot of sense if the thesis it goes with is that some such opinions are valid. So I don't think I misunderstood it.
- pekk 12y ago
  I don't have any problem with ML, nor do I favor Javascript or PHP. Maybe you shouldn't make so many assumptions.

hawkice 12y ago

I have always gotten the impression there was a failure of communication when (without lose of generality) Haskell programmers would tell (also, without loss of generality) Python programmers that Python only has one type, 'object', which appears to violate the understanding of the Python programmer thoroughly enough that there isn't really even a conversation about what is meant by the comment. The first point dissolves this conversation (because clearly neither the Haskell nor Python programmers are confused about the execution of actual programs). Notably, it dissolves it in a way where that pesky third issue doesn't pop up (which is perhaps the worst of them all, sans _maybe_ the last).

hcarvalhoalves 12y ago
Well, that's an interesting comment. I have almost a decade experience in Python, and having recently picked up Haskell, I clearly see the value of having (or not) a static type system. I have noticed that during all these years I would just "type-check" the various APIs in my mind, or with the aid of the REPL, but it's not as easy when programmers with less experience join the project. I would often have to explain tracebacks about type errors (e.g., tried to call a missing method on `None`, but the programmer didn't expect that API to return `None`). Strong typing avoids errors from propagating, but without static checking only gets you half-way there. I would still use Python (or other dynamic language) to introduce someone to programming - not having to reason about types lowers some barriers - but nowadays I'm not sure it pays off for a project expected to be maintained.
- crdoconnor 12y ago
  I was always on the fence about static typing because I figured that it automatically led to more verbose code (clearly a significant down side), but after looking at Haskell and F# I'm not so sure that's true for them, even though it definitely is for C++ and Java. I'm still unconvinced that additional testing is required to overcome bugs that a static type checker would catch, though. In my experience all of those "call a missing method on None" issues get caught relatively quickly by a test that you would have to write anyway even if you were using a language with static typing.

zak_mc_kracken 12y ago

> If somebody stays away from typed languages, it doesn't mean they're stupid, or lack education, or are afraid of maths. There are entirely valid practical reasons for staying away. Please drop the condescending tone. Well, ok, let's hear these practical reasons? Otherwise, it's just an empty claim.

eru 12y ago
Legacy code (and skillsets) are always a good practical reason.

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 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
  - 12y ago

tel 12y ago

With deference to Dr Kell, I think this is overwrought. He has some good points, points made happily against a particular form of "type cultist" who oversimplifies argument toward making types out to be something magical. They're not, no sane person would think so, but they are a static, syntactic proof system pertaining to the meaning of your programs and there's a lot to be said for such technology. I am happy to quibble exact points made in this rant, but I'm on my phone so for now I'll merely say that there's a large design space of programming languages and a similarly large (perhap today larger) space of type theories. Matching them up to hit all of your tradeoffs is hard, but there have been some great successes and I would happily contend that any professional programmer owes it to themselves to explore this design space "in anger". I'm also happy to generally claim that faster, more complete feedback is better than the opposite. Static systems of all regards are faster than "dynamic" ones, and most of them are more complete. This is where you hear about comparisons of types (especially dependent ones) and tests. It's great stuff to think about and explore. Further, I want to emphasize that SMT solvers are fascinating too and nobody thinks that they're not. The style of proof they provide is more expressive and less certain, though, so the right answer is to know how to combine all of these modes of evidence.

sanderjd 12y ago

> Type checkers are one way to gain assurance about software in advance of running it. Wonderful as they can be, they're not the only one. This is true, but in my experience they are far and away the most common and easily tooled automatic way. Tests may run automatically, but they must be manually written, and static analysis tools are not (yet?) very widespread.

colanderman 12y ago

No, I think a separate type-level language is a good thing, so long as my data-level language remains Turing complete (and thus undecidable). I would much rather be forced by the syntax -- by the construction of the language itself -- into a guaranteed decidable subset, rather than have to reason things out myself and get frustrated when the compiler doesn't agree with me (or when it used to agree with me and doesn't any longer!). Now, there's no reason that the type-level language can't be exactly a subset of the data-level language. I'd just rather not play guess-and-check decidability with the compiler the same way I currently have to play guess-and-check optimizability.

marvy 12y ago
I think the author meant that you don't want two separate Turing-complete languages, one for values at runtime, and another for values at compile time.
eru 12y ago
There are good arguments for not even getting Turing-completeness in your value-level language. Totality would be a nice goal. See http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html
- colanderman 12y ago
  Oh I totally agree. Unfortunately for many that's far too radical a notion, despite how unnecessary Turing-completeness is for 99.95% of programs written, and how desirable termination is. First you have to convince the Ruby/Python/JS/Elixir crowd of the frivolity of code mutability.

breckinloggins 12y ago

Things that also get my goat (from a less type theoretic point of view): - Assuming that type checking is the only thing you might want to do with your program at compile time. There are, in fact, arbitrarily many things you might want to do at compile time. Textual preprocessing, expansion macros, type checking, C++ template metaprogramming, etc. are all obvious examples. The fact that most languages bolt all of these things on as one-off features is a sign that something deeper is being missed (perhaps the 3-Lisp[1] idea, for example, or just consider plain ol' Lisp macros). - Assuming that totality, soundness, and lack of side effects are always type checking virtues. Sometimes I'd like a "typechecker" that isn't always guaranteed to terminate. Sometimes I'd like my typechecker to launch some missiles. This is really more about the previous point. - Assuming that type checking is NOT desired at runtime. Sometimes it is. Clojure's core.typed has the property that it is "just code" and can therefore be run at anytime and used for things other than checking that your code is safe to ship. [2] - Assuming that a program that fails type checking shouldn't be run. Maybe it should and the parts of the program that fail type checking should be run inside some monadic context. Maybe we want not only gradual typing, but gradual enforcement. Maybe if we had richer type data, then "failing type checking" wouldn't be binary. Perhaps a program that fails certain type checks has to add runtime support to enable certain features, but if the same program type checked to be about pure memory locations, the runtime would vanish and a "straight to the metal" program would remain. (In other words, maybe what we currently call a language's "runtime" should just be a residue of things that couldn't be checked at compile time, among other things.) - Assuming that types and the type checker should be a fixed feature of the language. Perhaps type checking should be something that is built as a library from language primitives. Take this far enough and you get something like exotypes. [3] Which reminds me... - Assuming that "type" is the only kind of metadata you might like to attach to a symbol, expression, or value. There are many other things I might like to express, and I might like to use the usual machinery of type checking to analyze or work with those things. Clojure's value-level metadata and Common Lisp's property lists are some good examples of generalizing this. - Focusing on manifest typing for verifiability of programs and ignoring the extra information it gives tooling. Visual Studio's IntelliSense and F#'s type providers are examples. At least one person at Microsoft has trouble sleeping at night because he or she is worrying about when the rest of us are going to figure this one out. [4] - Assuming that most programmers want one or the other. The article touched on this, but I wanted to expound a bit. I would like my original prototype to feel like play-doh and my finished product to feel like concrete. Why do I have to do this in two different languages? "Oh I'll prototype it in python and then switch to Haskell when I want it to be safe." What? - In general, assuming that it is the job of the language designer to provide the safety nets, rather than the DSL or API designer. A suitably designed programming language is one that could prevent operation Foo in layer 3 while allowing it in layers 1 and 2. This is one reason why languages like Idris are so complicated. Dependent types HAVE to be complicated because the language designer feels that it is his or her job to make sure the part of your program that runs at compile time terminates and doesn't do anything "bad". Why do we rarely question this assumption? [1] http://lisp-univ-etc.blogspot.com/2012/04/lisp-hackers-pascal-costanza.html http://lisp-univ-etc.blogspot.com/2012/04/lisp-hackers-pasca... [2] https://github.com/clojure/core.typed https://github.com/clojure/core.typed [3] http://dl.acm.org/citation.cfm?id=2594307 http://dl.acm.org/citation.cfm?id=2594307 [4] http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type-providers-in-pictures.aspx http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type...

cbd1984 12y ago

> It's also nothing to do with static checking—“type safety” holds in all “dynamically typed” languages. This. Exactly true, and often forgotten. It's useful here to distinguish between conversions and casts. Conversions use type information to ensure computations remain sensical; the canonical example is a conversion between integers and floating-point values which makes sure you never end up feeding invalid bit patterns into the relevant arithmetic hardware. An example of a cast is taking a bit pattern you had been treating as an integral value and then telling the language it's a floating-point value, and there not being an error at that point. Conversions don't break the type system; they use the type system. Casts throw types away.

kyllo 12y ago
Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload.
- dllthomas 12y ago
  Arguably, there is an intersection of "cast" and "conversion" where casts are valid.
- cbd1984 12y ago
  > Casts don't only throw types away, they can also add type information to otherwise untyped input, such as reading data from a file or an HTTP request payload. This is true. A more interesting example might be a program which creates database queries from user input casting input strings to the type "unescaped string", and then converting them to type "escaped string" by performing a string-escaping process on them. (A cast from "unescaped string" to "escaped string", which is done implicitly very often in languages where those types are not machine-checkable, is often disastrous.)
  - kyllo 12y ago
    Right, but I don't think this sort of type "conversion" (e.g. some function with type signature like this in Haskell) escapeQueryString :: ByteString -> Query is really adding or throwing away type information, it's just a function that accepts one type and returns another type. So it's not related to casting, except that it's the opposite of casting. But what that gives you is the ability to compose it with any other function that you define as accepting a `Query` type, and the program will refuse to compile if you ever accidentally try to pass it a ByteString. So it's about enforcing an invariant, in other words.

michaelochurch 12y ago

The hardest objective problem in computer science may be P ?= NP, but the hardest subjective problem is whether it is better to have static vs. dynamic typing in languages. There are extremely intelligent, thoughtful people on both sides... and it's rare in software engineering that there is such an even divide. I'm quite familiar with Haskell, Scala, Clojure, and many other languages... and I still can't conclusively call one better. I prefer static, on a mix of practical grounds, but I realize that it's not a clear victory. Take the concept of data frames from R, also seen in Python's Pandas library, and probably inspired by the APL family's (column-oriented) tables. It's not a complex concept. Yet it's very powerful for interactive data exploration. It's also a bitch to statically type (see: https://github.com/acowley/Frames https://github.com/acowley/Frames). It's more of a leap than lenses (and probably, like lenses, extremely cool once you fully "get" it). If we have to pull out some advanced Haskell extensions to do something basic in interactive data analysis then I consider that worrying. (This is not to say that Frames isn't a great piece of work. Bringing subtyping into a Hindley-Milner derived language and not having everything go to hell is really hard. See: Scala) And remember, this is coming from someone who's pretty invested in the "static" side. Clojure also has a world-class aesthetic sense. Haskell is still using camelCase. OCaml uses under_scores; that's better than fuckingUglyCamelCase, but not ideal. Clojure (and the Lisp family in general) is run by people who realize that aesthetics are really important and that allowing hyphenated-tokens is far better than allowing people who hate their space bars to write "a-1" when they should be writing "a - 1". That's just one example. For another, maps. Clojure has {"five" 5, "ten" 10} but Haskell has fromList [("five", 5), ("ten", 10)]. My point is that (which I prefer Haskell, for its types) Clojure's aesthetic sense is arguably better, and I would say world-class, especially considering that it runs on a butt-ugly platform (JVM) and is still a beautiful language. We need to keep watching that community closely because they're doing some great work in a wide variety of fields, including front-end development (ClojureScript). Type systems don't just make you write annotations; they force you to structure your code around type-checkability. This is inevitable, since type checking is by definition a specific kind of syntactic reasoning. There is some truth around that. Just to get data frames, you need row types which means you have subtyping, and that complicates type checking considerably. Haskell (see Frames) uses multiple "experts only" language extensions to get something that "just works" for casual use but requires advanced knowledge to grok the types. It's great work, but its difficulty shows that we can't just ignore subtyping. The counter-argument that I'd make is that 95+ percent (maybe more?) of all functions that are ever written ought to have simple static types. So much of code, when it is clean, is already well-typed, even in a dynlang. The difference is that, in a static language, the compiler yells any time someone fucks that up in refactoring. And, more generally, you learn about errors (not all errors, but a surprising percentage of them) sooner and that's a good thing. In a dynamically typed language, you see a lot of functions that evolve into multimethods that do different things per input type(s) and (although usually this won't happen if the code is maintained by decent designers) you can get O(n2) or worse complexity in the functionality. If you're programming defensively in a dynlang, you have to think about all the crap that might be passed into your functions. "What's a Matrix plus a Scalar? How about a RowVector plus a ColumnVector? How about a Sparse2DArray plus a DataFrame?" On the whole, I'd rather be in a statically-typed language for a program of any size, and I'm stodgy and conservative and old (but efficient and concise) so, for me, "big code" starts around a couple thousand lines. I hate writing boilerplate unit tests that a compiler and a type system would knock out automatically. But I do have to give Clojure a lot of props for its community and its aesthetic sense, and I think that the above obviously derive from its ease-of-use and its Lisp heritage, both of which are tied to a feature (dynamic typing) that I otherwise wouldn't much like. The main question that I've been pondering for a few years (and not coming to satisfactory answers) is whether it's possible to unify the cleanness-of-language and aesthetics of Clojure/Lisp with the static typing of Haskell... and not get some hyper-complex type system that results in compile-speed problems at scale (e.g. Scala under typical use). It's an open problem.

eru 12y ago

> (It should also do so using a straightforward explanation, ideally featuring a counterexample or stripped-down unprovable proposition. I don't know any type checker that does this, currently.) I guess the incomplete-pattern-matching warnings (in eg ghc) come closest. They usually give you an example of an example of a value you haven't matched. But that's a very restricted and simple domain.

fsloth 12y ago

I think the argumentation here is a bit a skewed towards 'what static types can and cannot do for the compiler' - i.e. how they can help the computer in constructing formal proofs. For me another almost as valuable thing is how static types help me think about and design the code. The static type information is always there to remind "this entity belongs to this set of objects" which frees me from the cognitive burden of maintaining this constantly in my working memory. With specific static types the function signatures now document the tranforms defined for those entities . This aspect of static types as a cognitive tool is highly personal, and not same for everyone, unlike the language and the compiler, though.

wyager 12y ago

I emphatically reject the many of the conclusions of this article. >Let me say it simply. Type systems cannot be a one-stop solution for specification and verification. Wrong! Any correctness property can be encoded into a sufficiently powerful type system. Which brings me to... >Curry-Howard is an interesting mathematical equivalence, but it does not advance any argument about how to write software effectively. This is absurd, of course. The isomorphism between type systems and proof systems allows us to build lots of impressive systems like Agda and Coq. >No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments. That's actually quite a reasonable desire. >Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code. To the author, this seems to mean "therefore, we shouldn't have types!". In reality, a sufficiently flexible programming language allows you to write type-level code in the same language as value-level code. See Agda. >Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic. Lots of people have typed transducers just fine... http://blog.podsnap.com/ducers2.html http://blog.podsnap.com/ducers2.html http://conscientiousprogrammer.com/blog/2014/08/07/understanding-cloure-transducers-through-types/ http://conscientiousprogrammer.com/blog/2014/08/07/understan...

djur 12y ago
> To the author, this seems to mean "therefore, we shouldn't have types!". This doesn't follow from the author's earlier statements about using and benefitting from languages with static type checkers. An ideal typed Lisp dialect would fit the author's requirements.
- jroesch 12y ago
  An ideally typed Lisp would be no different then a dependently typed language semantically. Yes, you would use slightly different syntax but a key feature of most dependently typed languages is that they only have a single class of pseudo-terms that are used for both types and programs. An example Idris program: double : Nat -> Nat double n = 2 * n ourVectorType : Type ourVectorType = Vect (double 1) Int aVector : ourVectorType aVector = [1, 2] If you change everything above to an S-Exp you have a typed Lisp where both types and terms have the same language.

mercurial 12y ago

> The Sniveley/Laucher talk included a comment that people like dynamic languages because their syntax is terse. Sure. Trying to have a strongly-typed Java program, for instance, means a lot of boilerplate. As a consequence, it's often not done, or at least not done enough. > To suggest that any distaste for types comes from annotation overhead is a way of dismissing it as a superficial issue. On a large codebase, there is nothing superficial about it. The more boilerplate you have, the more difficult it becomes to understand the codebase and to find code which actually does something. > If everyone would just use a modern language with a fancy type system, all our correctness problems would be over, right? If you believe this, you've drunk far too much Kool-Aid. Yet, apparently our profession is full of willing cult members. Let me say it simply. Type systems cannot be a one-stop solution for specification and verification. They are limited by definition. They reason only syntactically, and they specify only at the granularity of expressions. They're still useful, but let's be realistic. Let's be realistic, and not pretend this is a widespread opinion. > Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic. Usually they are captured only overapproximately, which, in turn, yields an inexpressive proof system. The end result is that some manifestly correct code does not type-check. Possibly, but it's all a question of tradeoffs. There is a lot more incorrect than correct code which doesn't typecheck.

mateuszf 12y ago
> On a large codebase, there is nothing superficial about it. The more boilerplate you have, the more difficult it becomes to understand the codebase and to find code which actually does something. In case of types it's true for humans. IDE will be able to build a very precise model and ease navigation and code changes when it understands types.
- superuser2 12y ago
  Why should this be a property of the IDE and not the language itself? No, seriously. If the language sucks but your interaction with the IDE is fine, why not have a language that is closer to your interaction with the IDE to begin with, and use a text editor?

fsloth 12y ago

This topic of "what are static types good for" continued to bug me because I could not formulate a concrete answer to myself. I found the following Reddit discussion http://www.reddit.com/r/programming/comments/lirke/simple_made_easy_by_rich_hickey_video/ http://www.reddit.com/r/programming/comments/lirke/simple_ma... Which had eventually the specific thing I was after in a comment by Rich Hickey which helped to nail the concept I was after "Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system." Which is precisely why I enjoy types: Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism. Which, I think tells exactly what static types are good for: For those sort of problems that benefit from having a formal specification. There are a lot of programs that have this quality. So the argumentation is a bit skewed off. It should not be about whether static or dynamic types are better but more focus on what are those identifiable problem patterns where a dynamic type system helps programmer create more value than a static one and vice versa.

shadowfox 12y ago
> Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism. I think this is a valid point. But I am less convinced about the second part. I feel that better type systems do help one model the world better (while retaining the consistency checking that you mentioned). In my mind at least having more/better "type tools" is like having differently shaped pieces in your lego tool box. You can create better models for yourself, because the pieces allow you to. And the more experience you have with them, your modeling abilities also improve.
- fsloth 12y ago
  The Lego analogy is what I also often like to use :) ! " I feel that better type systems do help one model the world better" I agree. But then again, I prefer to start from scribbling mathematical proof mimicking pseudocode which is easily transferred then to statical types. Some people just bang something together, prototype on the IDE/REPL as they go on and they can probably finish faster than me and produce value. If this figure-this-out-while-coding person then has the craftmanship to clean up the code the result is often as good as with the paper-and-pen-first approach. For larger systems, however, I would claim that starting from careful design pays off more because the code-prototype can quickly get out of hands if there are too many abstractions and variables flying in the air at the same time. The 'formal' approach has pitfalls if applied without taste or experience, since, well, modeling for modelings sake can get out of hands at which point one has a shaking tower of abstraction generated from mental masturbation rather than anything of lasting value. This becomes pathological the minute it reaches production. I think we recognize it all has to do with the experience of the programmer and the dedication but craftmanship is very hard to formalize...

raiph 12y ago

Perl 6 elegantly blends static nominal typing and arbitrarily loose or tight dynamic constraints. The following slides were published a week or so ago and should demolish most folks' overly simplistic view that one or other is best or indeed that they don't play well together: http://jnthn.net/papers/2015-fosdem-static-dynamic.pdf http://jnthn.net/papers/2015-fosdem-static-dynamic.pdf