7 ms·

There is a persistent myth that "A Haskell program that compiles is correct by definition" Indeed it is "correct" in the sense that it has a very high likeliho

There is a persistent myth that "A Haskell program that compiles is correct by definition" Indeed it is "correct" in the sense that it has a very high likelihood (maybe 90% ?) of doing what the programmer intended (Unlike say C or C++ where the probability drops to about 50% for beginners) However, that is a poor definition of "correct". While it's true that a lot of huge consequences have occurred due to stupid errors like buffer overflows (unintended bug), there are equally disastrous bugs caused by intent - i.e. the programmer had no idea the code could fail. The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that

dmitriid 7y ago
I sometimes phrase it as “yeah, your program is correct because it’s type-checked, but who has checked that your types are correct”? With dependent types some of the logic will be coded in types, and we would need to check those.
- moomin 7y ago
  Indeed, that’s why Dan North, Liz Keogh, et al have been banging the requirements capture drum for the last ten/twenty years. Doesn’t mean it might not be useful.
- grumdan 7y ago
  At least now we are checking that two pieces of saying what we want a program to do match up. It's less likely to get both the implementation and specification (in the form of types) wrong. Whenever the program fails to type-check, it will make you think about both bugs in the type and bugs in the code, even if the latter is more likely.
  - dmitriid 7y ago
    Types can’t encode the specification fully, or require a lot of work to encode a specification (so most people will skip this work). The simplest example is very common banking and e-commerce logic which is basically a series of checks in the form: if <some piece of data retrieved at runtime at that particular moment> is consistent with <multiple other pieces whose number and relevance depends on that data retrieved at runtime from potentially multiple sources>.
- lmm 7y ago
  That's the same logic as not writing tests because your tests might have bugs in.
mrgriffin 7y ago
> there are equally disastrous bugs caused by intent - i.e. the programmer had no idea the code could fail. At least some of these sorts of bugs (depending on how you define "fail") are captured even in Haskell today by things like Maybe. In fact, if Haskell was total (like Idris) you wouldn't even be able to write a function that searches a list for an element with this type: find :: (a -> Bool) -> [a] -> a Because there's no way for you to magic an a out of nowhere in the empty list case (whereas laziness lets you use bottom). You could however write a buggy find over known non-empty lists because you could always return one of the known elements, types aren't a panacea. Dependent types go further and let you guarantee things like "zip only compiles for two lists of exactly the same length" which can be helpful in some circumstances (specifically in Haskell we use things like zip [0..] too often to want to change the function literally called zip, but you could imagine another name, perhaps zipExact as in the Safe library). I suspect you probably already know this and meant a different kind of failure, such as mathematically invalid (which you could probably encode via a sufficiently powerful type system), or a simple misunderstanding of the requirements (which you—as the misunderstander—obviously can't).
- ferzul 7y ago
  > whereas laziness lets you use bottom in principle, only if you can prove you don't use the result. there's nothing wrong with not calculating a value that doesn't exist.
- mruts 7y ago
  I can't have much experience with dependent types, but I don't see how a compiler could ever tell if zip took two lists of the same length. Don't dependent types happen at run-time? It seems like you would have to solve the halting problem for them to work at compile time.
  - chongli 7y ago
    I've been learning the dependently typed functional language Idris over the past few weeks. The type-safe zip over Vects (linked lists with a length in the type) is a canonical example of compile-time proof that they must be the same length: zip : Vect n a -> Vect n b -> Vect n (a, b) This type specifies that both Vects must be length n. If they are not equal in length, the code will not compile. In fact, this type is so narrowly specified that Idris can infer the entire implementation of the function from it. Don't dependent types happen at run-time? Dependent types in Idris occur at compile time and are erased as part of compilation. At runtime, those Vects do not carry around any length information. It seems like you would have to solve the halting problem for them to work at compile time. Idris addresses this by having a totality checker. Every function in Idris is marked as either total (known to halt, barring any bugs in the totality checker) or partial (possibly not halting). Only total functions are allowed in types. For example, the function append: append : Vect m a -> Vect n a -> Vect (m + n) a This type uses addition as a type level function. Since (+) for natural numbers (which m and n are) is proven to be total when Idris compiles the library where it's defined, Idris allows it to be used as a type level function. So how does the totality checker work? Wouldn't that purport to solve the halting problem? No, the totality checker in Idris isn't magic, it's conservative about what it considers to be total. In order for it to declare a function total, it must identify at least one argument that progresses towards a base case at every step. It can do this even with mutually recursive functions. In practice, if you write an interactive program in Idris, you can make every function total except for main, which presumably contains an infinite loop that checks for input forever.
Legogris 7y ago
> The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that You're completely correct in the first half of that but the languages really can help there. Dependent types can be a lot more expressive and capture finer details of your semantics than what you're probably used to. I simple example is the `pop` function of a List. In Python, you could put strings in a list element. With Java, you can enforce the type of element that goes in a list. In a language with dependent types, you can ensure at compile-time that `pop` can only be called on a non-empty list and returns a list of `length - 1`. I'd say the difference between Haskell and C are orders of magnitude, not just a difference between 50% (probably a lot lower) and 90% (which would require you to specify the entire contract, at some point you may end up reimplementing business logic inside the type signature at which point you could have bugs there too and you haven't won that much. You still need to use it right). In dependently types languages, it's not unheard of with type signatures longer than the implementation itself. There is of course no silver bullet, but expressive type systems can protect you against unintended behavior and significantly reduces the number of unit tests you'd need to write. BTW, buffer overflows etc are a bit orthogonal to this, as that's related to memory safety, not type safety.
- lonelappde 7y ago
  Can a dependently typed list be used in the common case where the length of the list is not known at compile time?
  - andreabedini 7y ago
    Yes, that’s the whole point of dependent types: types can depend on (runtime) values.
  - Legogris 7y ago
    Yes. Just like with generics, you can parametrize them, for example in Idris you have the type `Vect n a`, being a list of type `a` with length `n`. An append function could look like this: app : Vect n a -> Vect m a -> Vect (n + m) a app Nil ys = ys app (x :: xs) ys = x :: app xs ys Source: https://www.idris-lang.org/example/ https://www.idris-lang.org/example/
Felz 7y ago
The point of the type system is that you can express your intent through an invariant or property at one place (i.e. the "head" function can specify that it should never be used on an empty list) and propagate that outwards so that it's enforced at all times. This is more effective than trying to remember to always check the head function in every single place you ever try to get the first element of a list. Yes, you can still write a compiling but wrong program. But it will likely be pretty close to what you actually want it to do, and it's easier to notice the behavior is not what you expected in one place, enforce that behavior via types, and see where you went wrong through compiler errors.
- yakshaving_jgt 7y ago
  The craziest thing about this is that programmers will often think "well, this tech can't prevent every possible kind of bug, therefore it's useless and we may as well use Python/Ruby/JS/whatever". Programming usually happens in the context of a business, and the technology used has implications in a cost/benefit analysis. Being able to express invariants at the type level is cheaper for a business at scale.
  - jstimpfle 7y ago
    Programmers who think types let them express their invariants are often ignorant about the fact that expressing those invariants makes their program a mess, so much that they have to consider possibly mutually incompatible language extensions, or reduce modularity of their program to the point where it becomes a pain to compile and becomes hard to maintain, and might require a complete redesign at some point when a minor functional requirement is added... If you consider this huge overhead in development cost, maybe time is better spent in less intrusive ways of improving software reliability.
    - marceloabsousa 7y ago
      Sure, but it's about striking a balance between the type (specification) and the program (implementation). The myth mentioned is just something people say to beginners in Haskell but no experienced programmer truly believes - reason being again this balance. When you can express so much in your type system that the implementation can be mostly automated, you have shifted the semantic mess to a level above but have not really made any substantial progress. Still, it's undeniable that type systems are perhaps the only kind of formal methods who really made it to the mainstream software developer because they can be useful. What I find frustrating is that no one is really guiding the programmers in finding good patterns for achieving a healthy balance specially for code that needs to be maintained and adjusted to new use cases.
atc 7y ago
Your argument is flawed. You make an unsubstantiated claim about correctness: > Indeed it is "correct" in the sense that it has a very high likelihood (maybe 90% ?) and then you claim it's poor: > However, that is a poor definition of "correct". and therefore blame the language by implication. Furthermore, you make the false suggestion that the challenges: > How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" are mutually exclusive. In two words: amateur analysis.
marmaduke 7y ago
Really good point here: > How do I capture this extremely complicated real world semantics in code? This is why I keep using Python after having dabbled in other more interesting languages: the probability of writing correct code for me and the team I support is fairly high.
- 6thaccount2 7y ago
  Yea...my first language that I got really comfortable in was Python (used Matlab, Assembly, C, Basic...etc in college). I've since then dabbled in: C++, Ada, Rust, Nim, D, Haskell, OCaml, F#, C#, Java, Clojure, Scala, Kotlin, Common Lisp, Racket, PicoLisp, Groovy, Powershell, Bash, TCL, Julia, APL, Forth, J, Rebol, VBA...the list goes on. I've only ever gotten shallow in these languages, but have always found something missing (I'm sure others have said the same about Python, but I wanted to add my anecdotal experience). Out of all of those, I've pretty much stayed with Python as it keeps letting me get my job done with minimal code and maximum readability. I've been almost as efficient in Julia and have gradually picked up Powershell's quirks and find them all good for scripting tasks where you don't create too many pages of code. Would I migrate with a large codebase? It depends on the industry of course, but if it is common line of business applications I'd be hard pressed to find something else. I was really hoping Kotlin could help here with it's REPL/Scratchpad and being on the JVM, but I didn't end up being too impressed (it might take more time). I don't want to contribute to a static versus dynamic never ending argument. I guess I will say that Haskell, the JVM, and .NET just seem to have to much ceremony around them. I'm sure it's very powerful, but there is a lot to learn that distracts from just writing code.
bad_user 7y ago
You're building a strawman. I've never heard of that myth, the saying is more like "if a Haskell program compiles, it usually works". And you can say the same thing about a couple of other statically typed, functional programming languages. --- > "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that Actually languages can help a lot. This isn't just about "silly mistakes". Compilers are _theorem provers_. Quite literally there's an equivalence between type theory and mathematical logic. I hope you're not saying that math logic doesn't help in modeling real world semantics. So yes, via modelling types in an expressive language you can at least have proof that the changes you make are consistent with the world view you had before those changes. Of course people accustomed to less expressive languages like Java won't believe this until they see it. But you should really look into Haskell to see the difference. And dependent typing brings this to the next level.
- 6thaccount2 7y ago
  Ada with Spark is pretty cool.
  - jcadam 7y ago
    I used Ada for a few years back when I was working on satellite programs. It's the closest thing to a "If it compiles, it probably works" language that I've ever seen.
    - 6thaccount2 7y ago
      I really wish you could use all of the adacore stuff for free in commercial closed source software and just pay for IDE support and maybe some specific libraries.
conjectures 7y ago
> "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that This isn't true. It's possible to write a symbolic differentiation system using, primarily, Scala's type system. In an elegant fashion. Similarly, Julia represents math better than, say python or Java. A vector type should not need to know about inner products of vectors, because the math definition of a vector space does not. This will have large effects on how easy it is to decompose your code into neat little pieces.
namelosw 7y ago
It probably "A Haskell program compiles does not crash if you don't use a specific set of functions". But it probably could be true for a lot of languages, but for Haskell, the set is much smaller Dependent type can let you achieve some degree of semantic correctness above that. Either by refined types or proof. But it's not generally applied because there are a lot of things we just couldn't prove yet.
dgb23 7y ago
> The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that. Probably a tangent but I feel like this is only partly true. DSLs are specifically built to do that for example. The languages can meet us half-way so to speak.
whateveracct 7y ago
The point is that Haskell allows you to push more business logic to the proposition (type) level. Nobody actually thinks Haskell programs can't include mistakes. Dependent types aim to address exactly "How do I capture this extremely complicated real world semantics in code?". Except now you have the option to capture some or all of those semantics in types instead of terms.
zmmmmm 7y ago
> but rather "How do I capture this extremely complicated real world semantics in code?" I'm not sure that's even it. It's "I don't really understand the requirements until I try to implement them and therefore my first 6 attempts are hopelessly wrong". The reason dynamic languages are so popular I think is because they make it so fast to iterate through the first 6 attempts whereas statically typed languages make that 50% slower and that generates a huge feeling of helplessness and frustration that you keep doing all this work to satisfy the compiler and then its thrown away. Of course one can argue that all these people are stupid and should just understand the requirements in the first place, but it's a separate point: that is reality - people find it hard to understand requirements. But it is one reason I like more "incremental" languages like Groovy since I can iterate really fast in dynamic mode and then tighten up all the screws afterwards by converting it to statically typed code.

dmitriid 7y ago

I sometimes phrase it as “yeah, your program is correct because it’s type-checked, but who has checked that your types are correct”? With dependent types some of the logic will be coded in types, and we would need to check those.

moomin 7y ago
Indeed, that’s why Dan North, Liz Keogh, et al have been banging the requirements capture drum for the last ten/twenty years. Doesn’t mean it might not be useful.
grumdan 7y ago
At least now we are checking that two pieces of saying what we want a program to do match up. It's less likely to get both the implementation and specification (in the form of types) wrong. Whenever the program fails to type-check, it will make you think about both bugs in the type and bugs in the code, even if the latter is more likely.
- dmitriid 7y ago
  Types can’t encode the specification fully, or require a lot of work to encode a specification (so most people will skip this work). The simplest example is very common banking and e-commerce logic which is basically a series of checks in the form: if <some piece of data retrieved at runtime at that particular moment> is consistent with <multiple other pieces whose number and relevance depends on that data retrieved at runtime from potentially multiple sources>.
lmm 7y ago
That's the same logic as not writing tests because your tests might have bugs in.

mrgriffin 7y ago

> there are equally disastrous bugs caused by intent - i.e. the programmer had no idea the code could fail. At least some of these sorts of bugs (depending on how you define "fail") are captured even in Haskell today by things like Maybe. In fact, if Haskell was total (like Idris) you wouldn't even be able to write a function that searches a list for an element with this type: find :: (a -> Bool) -> [a] -> a Because there's no way for you to magic an a out of nowhere in the empty list case (whereas laziness lets you use bottom). You could however write a buggy find over known non-empty lists because you could always return one of the known elements, types aren't a panacea. Dependent types go further and let you guarantee things like "zip only compiles for two lists of exactly the same length" which can be helpful in some circumstances (specifically in Haskell we use things like zip [0..] too often to want to change the function literally called zip, but you could imagine another name, perhaps zipExact as in the Safe library). I suspect you probably already know this and meant a different kind of failure, such as mathematically invalid (which you could probably encode via a sufficiently powerful type system), or a simple misunderstanding of the requirements (which you—as the misunderstander—obviously can't).

ferzul 7y ago
> whereas laziness lets you use bottom in principle, only if you can prove you don't use the result. there's nothing wrong with not calculating a value that doesn't exist.
mruts 7y ago
I can't have much experience with dependent types, but I don't see how a compiler could ever tell if zip took two lists of the same length. Don't dependent types happen at run-time? It seems like you would have to solve the halting problem for them to work at compile time.
- chongli 7y ago
  I've been learning the dependently typed functional language Idris over the past few weeks. The type-safe zip over Vects (linked lists with a length in the type) is a canonical example of compile-time proof that they must be the same length: zip : Vect n a -> Vect n b -> Vect n (a, b) This type specifies that both Vects must be length n. If they are not equal in length, the code will not compile. In fact, this type is so narrowly specified that Idris can infer the entire implementation of the function from it. Don't dependent types happen at run-time? Dependent types in Idris occur at compile time and are erased as part of compilation. At runtime, those Vects do not carry around any length information. It seems like you would have to solve the halting problem for them to work at compile time. Idris addresses this by having a totality checker. Every function in Idris is marked as either total (known to halt, barring any bugs in the totality checker) or partial (possibly not halting). Only total functions are allowed in types. For example, the function append: append : Vect m a -> Vect n a -> Vect (m + n) a This type uses addition as a type level function. Since (+) for natural numbers (which m and n are) is proven to be total when Idris compiles the library where it's defined, Idris allows it to be used as a type level function. So how does the totality checker work? Wouldn't that purport to solve the halting problem? No, the totality checker in Idris isn't magic, it's conservative about what it considers to be total. In order for it to declare a function total, it must identify at least one argument that progresses towards a base case at every step. It can do this even with mutually recursive functions. In practice, if you write an interactive program in Idris, you can make every function total except for main, which presumably contains an infinite loop that checks for input forever.

Legogris 7y ago

> The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that You're completely correct in the first half of that but the languages really can help there. Dependent types can be a lot more expressive and capture finer details of your semantics than what you're probably used to. I simple example is the `pop` function of a List. In Python, you could put strings in a list element. With Java, you can enforce the type of element that goes in a list. In a language with dependent types, you can ensure at compile-time that `pop` can only be called on a non-empty list and returns a list of `length - 1`. I'd say the difference between Haskell and C are orders of magnitude, not just a difference between 50% (probably a lot lower) and 90% (which would require you to specify the entire contract, at some point you may end up reimplementing business logic inside the type signature at which point you could have bugs there too and you haven't won that much. You still need to use it right). In dependently types languages, it's not unheard of with type signatures longer than the implementation itself. There is of course no silver bullet, but expressive type systems can protect you against unintended behavior and significantly reduces the number of unit tests you'd need to write. BTW, buffer overflows etc are a bit orthogonal to this, as that's related to memory safety, not type safety.

lonelappde 7y ago
Can a dependently typed list be used in the common case where the length of the list is not known at compile time?
- andreabedini 7y ago
  Yes, that’s the whole point of dependent types: types can depend on (runtime) values.
- Legogris 7y ago
  Yes. Just like with generics, you can parametrize them, for example in Idris you have the type `Vect n a`, being a list of type `a` with length `n`. An append function could look like this: app : Vect n a -> Vect m a -> Vect (n + m) a app Nil ys = ys app (x :: xs) ys = x :: app xs ys Source: https://www.idris-lang.org/example/ https://www.idris-lang.org/example/

Felz 7y ago

The point of the type system is that you can express your intent through an invariant or property at one place (i.e. the "head" function can specify that it should never be used on an empty list) and propagate that outwards so that it's enforced at all times. This is more effective than trying to remember to always check the head function in every single place you ever try to get the first element of a list. Yes, you can still write a compiling but wrong program. But it will likely be pretty close to what you actually want it to do, and it's easier to notice the behavior is not what you expected in one place, enforce that behavior via types, and see where you went wrong through compiler errors.

yakshaving_jgt 7y ago
The craziest thing about this is that programmers will often think "well, this tech can't prevent every possible kind of bug, therefore it's useless and we may as well use Python/Ruby/JS/whatever". Programming usually happens in the context of a business, and the technology used has implications in a cost/benefit analysis. Being able to express invariants at the type level is cheaper for a business at scale.
- jstimpfle 7y ago
  Programmers who think types let them express their invariants are often ignorant about the fact that expressing those invariants makes their program a mess, so much that they have to consider possibly mutually incompatible language extensions, or reduce modularity of their program to the point where it becomes a pain to compile and becomes hard to maintain, and might require a complete redesign at some point when a minor functional requirement is added... If you consider this huge overhead in development cost, maybe time is better spent in less intrusive ways of improving software reliability.
  - marceloabsousa 7y ago
    Sure, but it's about striking a balance between the type (specification) and the program (implementation). The myth mentioned is just something people say to beginners in Haskell but no experienced programmer truly believes - reason being again this balance. When you can express so much in your type system that the implementation can be mostly automated, you have shifted the semantic mess to a level above but have not really made any substantial progress. Still, it's undeniable that type systems are perhaps the only kind of formal methods who really made it to the mainstream software developer because they can be useful. What I find frustrating is that no one is really guiding the programmers in finding good patterns for achieving a healthy balance specially for code that needs to be maintained and adjusted to new use cases.

atc 7y ago

Your argument is flawed. You make an unsubstantiated claim about correctness: > Indeed it is "correct" in the sense that it has a very high likelihood (maybe 90% ?) and then you claim it's poor: > However, that is a poor definition of "correct". and therefore blame the language by implication. Furthermore, you make the false suggestion that the challenges: > How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" are mutually exclusive. In two words: amateur analysis.

marmaduke 7y ago

Really good point here: > How do I capture this extremely complicated real world semantics in code? This is why I keep using Python after having dabbled in other more interesting languages: the probability of writing correct code for me and the team I support is fairly high.

6thaccount2 7y ago
Yea...my first language that I got really comfortable in was Python (used Matlab, Assembly, C, Basic...etc in college). I've since then dabbled in: C++, Ada, Rust, Nim, D, Haskell, OCaml, F#, C#, Java, Clojure, Scala, Kotlin, Common Lisp, Racket, PicoLisp, Groovy, Powershell, Bash, TCL, Julia, APL, Forth, J, Rebol, VBA...the list goes on. I've only ever gotten shallow in these languages, but have always found something missing (I'm sure others have said the same about Python, but I wanted to add my anecdotal experience). Out of all of those, I've pretty much stayed with Python as it keeps letting me get my job done with minimal code and maximum readability. I've been almost as efficient in Julia and have gradually picked up Powershell's quirks and find them all good for scripting tasks where you don't create too many pages of code. Would I migrate with a large codebase? It depends on the industry of course, but if it is common line of business applications I'd be hard pressed to find something else. I was really hoping Kotlin could help here with it's REPL/Scratchpad and being on the JVM, but I didn't end up being too impressed (it might take more time). I don't want to contribute to a static versus dynamic never ending argument. I guess I will say that Haskell, the JVM, and .NET just seem to have to much ceremony around them. I'm sure it's very powerful, but there is a lot to learn that distracts from just writing code.

bad_user 7y ago

You're building a strawman. I've never heard of that myth, the saying is more like "if a Haskell program compiles, it usually works". And you can say the same thing about a couple of other statically typed, functional programming languages. --- > "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that Actually languages can help a lot. This isn't just about "silly mistakes". Compilers are _theorem provers_. Quite literally there's an equivalence between type theory and mathematical logic. I hope you're not saying that math logic doesn't help in modeling real world semantics. So yes, via modelling types in an expressive language you can at least have proof that the changes you make are consistent with the world view you had before those changes. Of course people accustomed to less expressive languages like Java won't believe this until they see it. But you should really look into Haskell to see the difference. And dependent typing brings this to the next level.

6thaccount2 7y ago
Ada with Spark is pretty cool.
- jcadam 7y ago
  I used Ada for a few years back when I was working on satellite programs. It's the closest thing to a "If it compiles, it probably works" language that I've ever seen.
  - 6thaccount2 7y ago
    I really wish you could use all of the adacore stuff for free in commercial closed source software and just pay for IDE support and maybe some specific libraries.

conjectures 7y ago

> "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that This isn't true. It's possible to write a symbolic differentiation system using, primarily, Scala's type system. In an elegant fashion. Similarly, Julia represents math better than, say python or Java. A vector type should not need to know about inner products of vectors, because the math definition of a vector space does not. This will have large effects on how easy it is to decompose your code into neat little pieces.

namelosw 7y ago

It probably "A Haskell program compiles does not crash if you don't use a specific set of functions". But it probably could be true for a lot of languages, but for Haskell, the set is much smaller Dependent type can let you achieve some degree of semantic correctness above that. Either by refined types or proof. But it's not generally applied because there are a lot of things we just couldn't prove yet.

dgb23 7y ago

> The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that. Probably a tangent but I feel like this is only partly true. DSLs are specifically built to do that for example. The languages can meet us half-way so to speak.

whateveracct 7y ago

The point is that Haskell allows you to push more business logic to the proposition (type) level. Nobody actually thinks Haskell programs can't include mistakes. Dependent types aim to address exactly "How do I capture this extremely complicated real world semantics in code?". Except now you have the option to capture some or all of those semantics in types instead of terms.

zmmmmm 7y ago

> but rather "How do I capture this extremely complicated real world semantics in code?" I'm not sure that's even it. It's "I don't really understand the requirements until I try to implement them and therefore my first 6 attempts are hopelessly wrong". The reason dynamic languages are so popular I think is because they make it so fast to iterate through the first 6 attempts whereas statically typed languages make that 50% slower and that generates a huge feeling of helplessness and frustration that you keep doing all this work to satisfy the compiler and then its thrown away. Of course one can argue that all these people are stupid and should just understand the requirements in the first place, but it's a separate point: that is reality - people find it hard to understand requirements. But it is one reason I like more "incremental" languages like Groovy since I can iterate really fast in dynamic mode and then tighten up all the screws afterwards by converting it to statically typed code.