8 ms·

Has anyone here shipped anything production worthy with dependently typed languages? I'm serious. There are like 10 PhDs in France working on a certified compil

Has anyone here shipped anything production worthy with dependently typed languages? I'm serious. There are like 10 PhDs in France working on a certified compiler toolchain for C and that's it. Meanwhile Go and JavaScript are taking over the world and they're anything but dependently typed. Maybe there's a reason for that? Maybe the reason is that after a certain point the validation overhead of advanced type systems is just not worth it. Yes, I know the article isn't about dependent types per se but many of the features he wants get pretty close to dependent types since that is pretty much the state of the art when it comes to advanced type systems with lawful abstractions and whatnot.

Ixiaus 11y ago
I'm shipping massive amounts of code written in Haskell - production worthy for a real product - and the benefits of using Haskell over any other mainstream imperative language have been fairly significant.
- Drup 11y ago
  Haskell is not a real dependently type language. It may tries to quack like one, but compared to Idris/Agda, it's doing a very bad job at it. I'm pretty sure Parent didn't included Haskell.
  - wyager 11y ago
    Haskell has decent experimental support for dependent types. I've been using the CLaSH Haskell to hardware conversion system, which makes heavy use of type level arithmetic, with pretty good results.
    - Drup 11y ago
      Type level arithmetic is sugar for clever GADTs, not full blown dependent types. Try to do things in Agda/Idris and come back to haskell, the expressiveness is not nearly comparable.
      - wyager 11y ago
        Are Nats in agda and idris not also just GADT based peano numbers?
        Drup 11y ago
        The toyish version showed in tutorials, yes. The real stuff, no, it's just .. integers. And anyway, my point was that you can do much much more than type level arithmetic.
  - Ixiaus 11y ago
    His comparison sounded much more like "research languages vs. mainstream imperative languages" and Haskell definitely came from research land, just as Idris and Agda are. Plus someone is seriously working on dependent types in Haskell - so no, I think it's fitting.
jjaredsimpson 11y ago
The value proposition I've always read is related to gains in expressiveness and correctness. Programming is eventually going to become like Advanced Chess (human+computer team) and entire classes of mistakes will cease to exist. I don't think I can be convinced that correct-by-construction methods are wrongheaded. I am convinced that humans aren't very good at wrangling precise and complex and large ideas without failure.
Drup 11y ago
Does selling CompCert to Airbus count as begin "production worthy" ? I would (not) be amused when people try to put javascript in plane navigation systems. Do not forget that most dependently type languages (and Coq the first) are proof languages. The goal is not (only) to write programs, but to prove things and a rather large number of theorem have been proven that way. Dependently types languages for programming (as opposed to proving) are very much cutting edge research. Is it so surprising that they are not used in the wild ? Edit: woops, missed the "here" in parent's comment. No, I don't work on compcert. :)
- theseoafs 11y ago
  > Dependently types languages for programming (as opposed to proving) are very much cutting edge research. Is it so surprising that they are not used in the wild ? How long will this be the case? Seems like they've been "cutting edge research" for a few decades, and the Curry-Howard correspondence itself is like 80 years old. Surely if there were a real demand for these kinds of programming languages, we would have seen some industry penetration at some point, right?
  - tunesmith 11y ago
    There's been plenty of industry penetration for languages with more advanced type systems. Not sure why there's the arbitrary line being drawn here of dependent type systems. Some of this is about the penetration of certain ideas. Like, we had to wait for multiple cores on commodity hardware before functional programming started to cross over from the academic community to the professional web programmer. That shift helps your average programmer to think a bit more mathematically, and then it's basically about whether the programmer starts to appreciate types - and to me that seems to be less about purity of argument than the professional atmosphere the programmer is in. Are you prototyping and moving fast and breaking stuff, or are you caring more about longevity and correctness. And then once you start getting more into static typing and functional programming, a lot of these other ideas start to become more attractive and intriguing. It's like a lot of ideas that circulate around for a long time before they really take hold; you're waiting for a certain critical mass of system inputs and momentum, and then things can start to change really fast.
mmarx 11y ago
The formally-verified Odd Order Theorem[0] using Coq was quite an acomplishment (though probably not what you had in mind). [0] https://hal.inria.fr/hal-00816699/file/main.pdf https://hal.inria.fr/hal-00816699/file/main.pdf
incepted 11y ago
Dependently type languages are wonderful in theory and a royal pain in the butt in practice. It's a great example of "devil in the details" kind of thing. For example, let's say you define a type of list of size n. Great. You can only assign list of the same size and you can only append an element of the type "n" to a type "n-1" or the compiler will complain. Now you can even prove that your program is formally correct. What's not to like? And then, reality knocks at your door. How do you instantiate such a type? It needs to be instantiated right away with n elements or your program won't compile. But these elements are coming from the runtime, say, a database. How the hell does this work? Dependently typed languages that go just a step beyond prototypes quickly realize how crippling this approach is and they will give you all kinds of escape hatches to weaken the type system just so you can use the darn thing. But it's futile, because at the end of the day, a program is a living thing that relies on side effects and external inputs, and sophisticated systems are just not designed to cope with human fuzziness. The reason why dependently typed systems never became popular is not because the world hasn't realized yet how awesome they are: it's because they just aren't a good fit to solve real problems.
- mjcohen 11y ago
  That's one of the reasons Pascal failed.
- geofft 11y ago
  I wish we (both potential users, and developers of these languages) would start seeing these things more like enhanced tests than perfect manifestations of mathematical truth. Nobody would ever question the value of a unit-testing framework because it requires you to instantiate objects and doesn't hit the database and the ORM. (Yes, there are testing strategies that cover all of that, but for unit-testing application logic, you generally want to skip all of that.) Dependent types should let you do the same thing that a test would do, except exhaustively: if you add a new email address to an account with N addresses, you can then index N+1 of those addresses, but no more. The N-address account coming from the ORM isn't considered an "escape hatch" that "weakens the test system": it's just how it works. I want stronger types for exhaustive testing of business logic on individual functions -- the sort of things that a comment would say (e.g. "Returns a subset of this parameter if it is provided, otherwise..."), except machine-checked. I don't need my entire program to have a type that Messrs. Curry and Howard like. In all probability, my entire program is structured as an infinite loop anyway. I don't know that any systems really let you get here (other than maybe extraction of particular functions into Haskell or ML, but really the people who would voluntarily write their entire app in Haskell or ML are not the right target audience).
mafribe 11y ago
after a certain point the validation overhead of advanced type systems is just not worth it. But what makes you think you need dependent types to do full specification and verification of a program? Instead you could use program logic. Write the program in any language you like and later, when it the program is finished verifiy that it meets its specification using program logic. This separates programming from verification completely. In my opinion this is the future of certified programming. Dependent types are too heavyweight to support any conventional programming process. Another advantage is that unlike Curry-Howard based verification, program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This tends to yield shorter proofs. See Microsoft's Daphny [1] or CFML [2] for prototype tool chains implementing program logic based verification. Facebook's infer tool [3], while not allowing full verification, is also based on program logic. [1] http://research.microsoft.com/en-us/projects/dafny http://research.microsoft.com/en-us/projects/dafny [2] http://www.chargueraud.org/softs/cfml http://www.chargueraud.org/softs/cfml [3] https://github.com/facebook/infer https://github.com/facebook/infer
- darzu 11y ago
  > This separates programming from verification completely. This is simply not the case. Significant verification projects always plan for verification and do verification in tandem. This is definitely true for all Dafny projects to date as well. Verification is just so much harder than unverified programming that you generally want to do everything you can while programming to make verification easier. This may become less true as proof automation improves but it will always be a tension. > But what makes you think you need dependent types to do full specification [...] ? Also, keep in mind that Dafny and similar tools can only express first order logic; this can significantly restricts the expressiveness of your specification language and intermediate lemmas. > program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This is a silly point. First off proof assistants like Coq aren't inconsistent with the law of the excluded middle (only NuPRL is I believe) so you can always assume it as an axiom if you'd like. Most projects don't do this because constructivism is a benefit not a burden in verification: it allows you to make distinctions that aren't possible in classical logic. I agree that Dafny and similar projects are very exciting though; Dafny's tight integration with Z3 provides an awesome level of automation that will keep getting better and better.
darzu 11y ago
True certified programming has a lot of overhead but there are definitely areas where it'll be worth it: medical devices, car systems, mars rovers, aviation, etc. The University of Washington is actively working on verifying radiation therapy machine software and early results are already used in production for example. I think the reason certified programming hasn't been more widely adopted yet is because the tooling is terrible at the moment and we still have some important bits of theory to work out (e.g. homotopy type theory & other equality issues). It'll get there. Projects like Lean & Dafny at MSR, Adam Chlipala's work at MIT, and the large amount of theory work being done at CMU, Cornell, UPenn, Inria and other places are very promising. My bet is that the tooling & theory will continue to improve and eventually the overhead will become low enough that a significant portion (~10-20%) of software will be certified. I recommend reading Adam Chlipala's vision statement for inspiration on what certified programming could enable: http://adam.chlipala.net/summary.html http://adam.chlipala.net/summary.html
jules 11y ago
The reason is twofold. One, research into dependent types is still ongoing. Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Well, arguably just a single construct: it generalizes the usual function type A -> B to the dependent function type x:A -> B(x). This subsumes a lot of things like generics, existential types, GADTs, higher kinded types, rank-n polymorphism, etc. You can even use it to do record types, polymorphic variants, modules, refinement types, etc. The dependent function type is a universal lego block for types. Even more striking, it unifies the type level with the value level. Instead of having a language of types and a language of expressions there is just one language. The type List<T> takes a type T and gives you the type of lists with elements of type T. In dependently typed languages this is just a function List(T) that takes a type and returns a type. Instead of having F<T> at the type level and f(x) at the value level, there's only one kind of function that does both. I have no doubt that we will eventually be programming in a dependently typed language, the only question is when.
- mafribe 11y ago
  I have no doubt that we will eventually be programming in a dependently typed language, the only question is when. For the reasons I give in another posting in this thread (inability to extend dependent types beyond pure functions, and forcing the full cost of verification on early states of software productions when specifications are unstable), I predict the opposite: dependently typed verification will give way to program logic, the only question is when.
  - jules 11y ago
    Why would dependent types not extend beyond pure functions? Idris has both dependent types and non pure functions, is that not satisfactory? The fact that you can write software that provably satisfies a strict specification in dependently typed languages doesn't mean that you must. It is perfectly possible to program in them like you would in a normal language. That's what I was trying to get at: dependent types are also more expressive, not just more constraining. Now that I know about dependent types I regularly run into situations where I think "gosh, if I had dependent types I wouldn't have had to put in these type casts or handle these error cases that I know for sure cannot happen". So even if you ultimately want to reason about your programs using an external program logic (which I predict we do not, but we'll see), then for expressiveness you still want your language to have dependent types for the reason I mentioned above: > Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system. You can write your program as normal and later prove lemmas about functions in the program. For instance instead of saying reverse : Vec n a -> Vec n a or reverse : (xs : List a) -> {ys : List a | length xs == length ys} you can do reverse : List a -> List a and a lemma reverse_preserves_length : forall xs. length (reverse xs) == length xs It's just not the only option you have. What's this forall you say? A dependent function type of course!
lmm 11y ago
I've been doing Scala for 5+ years, real-world production code. From here it feels like the popularity of types is going up and up (and within Scala they're becoming more popular e.g. look at doobie). Haskell and OCaml look to be getting more popular, not less. Javascript is a special case because of the browser. Go is mostly displacing Python and Ruby. There's certainly no exodus of ex-Haskell programmers fleeing for less typed languages.

Ixiaus 11y ago

I'm shipping massive amounts of code written in Haskell - production worthy for a real product - and the benefits of using Haskell over any other mainstream imperative language have been fairly significant.

Drup 11y ago
Haskell is not a real dependently type language. It may tries to quack like one, but compared to Idris/Agda, it's doing a very bad job at it. I'm pretty sure Parent didn't included Haskell.
- wyager 11y ago
  Haskell has decent experimental support for dependent types. I've been using the CLaSH Haskell to hardware conversion system, which makes heavy use of type level arithmetic, with pretty good results.
  - Drup 11y ago
    Type level arithmetic is sugar for clever GADTs, not full blown dependent types. Try to do things in Agda/Idris and come back to haskell, the expressiveness is not nearly comparable.
    - wyager 11y ago
      Are Nats in agda and idris not also just GADT based peano numbers?
      - Drup 11y ago
        The toyish version showed in tutorials, yes. The real stuff, no, it's just .. integers. And anyway, my point was that you can do much much more than type level arithmetic.
- Ixiaus 11y ago
  His comparison sounded much more like "research languages vs. mainstream imperative languages" and Haskell definitely came from research land, just as Idris and Agda are. Plus someone is seriously working on dependent types in Haskell - so no, I think it's fitting.

jjaredsimpson 11y ago

The value proposition I've always read is related to gains in expressiveness and correctness. Programming is eventually going to become like Advanced Chess (human+computer team) and entire classes of mistakes will cease to exist. I don't think I can be convinced that correct-by-construction methods are wrongheaded. I am convinced that humans aren't very good at wrangling precise and complex and large ideas without failure.

Drup 11y ago

Does selling CompCert to Airbus count as begin "production worthy" ? I would (not) be amused when people try to put javascript in plane navigation systems. Do not forget that most dependently type languages (and Coq the first) are proof languages. The goal is not (only) to write programs, but to prove things and a rather large number of theorem have been proven that way. Dependently types languages for programming (as opposed to proving) are very much cutting edge research. Is it so surprising that they are not used in the wild ? Edit: woops, missed the "here" in parent's comment. No, I don't work on compcert. :)

theseoafs 11y ago
> Dependently types languages for programming (as opposed to proving) are very much cutting edge research. Is it so surprising that they are not used in the wild ? How long will this be the case? Seems like they've been "cutting edge research" for a few decades, and the Curry-Howard correspondence itself is like 80 years old. Surely if there were a real demand for these kinds of programming languages, we would have seen some industry penetration at some point, right?
- tunesmith 11y ago
  There's been plenty of industry penetration for languages with more advanced type systems. Not sure why there's the arbitrary line being drawn here of dependent type systems. Some of this is about the penetration of certain ideas. Like, we had to wait for multiple cores on commodity hardware before functional programming started to cross over from the academic community to the professional web programmer. That shift helps your average programmer to think a bit more mathematically, and then it's basically about whether the programmer starts to appreciate types - and to me that seems to be less about purity of argument than the professional atmosphere the programmer is in. Are you prototyping and moving fast and breaking stuff, or are you caring more about longevity and correctness. And then once you start getting more into static typing and functional programming, a lot of these other ideas start to become more attractive and intriguing. It's like a lot of ideas that circulate around for a long time before they really take hold; you're waiting for a certain critical mass of system inputs and momentum, and then things can start to change really fast.

mmarx 11y ago

The formally-verified Odd Order Theorem[0] using Coq was quite an acomplishment (though probably not what you had in mind). [0] https://hal.inria.fr/hal-00816699/file/main.pdf https://hal.inria.fr/hal-00816699/file/main.pdf

incepted 11y ago

Dependently type languages are wonderful in theory and a royal pain in the butt in practice. It's a great example of "devil in the details" kind of thing. For example, let's say you define a type of list of size n. Great. You can only assign list of the same size and you can only append an element of the type "n" to a type "n-1" or the compiler will complain. Now you can even prove that your program is formally correct. What's not to like? And then, reality knocks at your door. How do you instantiate such a type? It needs to be instantiated right away with n elements or your program won't compile. But these elements are coming from the runtime, say, a database. How the hell does this work? Dependently typed languages that go just a step beyond prototypes quickly realize how crippling this approach is and they will give you all kinds of escape hatches to weaken the type system just so you can use the darn thing. But it's futile, because at the end of the day, a program is a living thing that relies on side effects and external inputs, and sophisticated systems are just not designed to cope with human fuzziness. The reason why dependently typed systems never became popular is not because the world hasn't realized yet how awesome they are: it's because they just aren't a good fit to solve real problems.

mjcohen 11y ago
That's one of the reasons Pascal failed.
geofft 11y ago
I wish we (both potential users, and developers of these languages) would start seeing these things more like enhanced tests than perfect manifestations of mathematical truth. Nobody would ever question the value of a unit-testing framework because it requires you to instantiate objects and doesn't hit the database and the ORM. (Yes, there are testing strategies that cover all of that, but for unit-testing application logic, you generally want to skip all of that.) Dependent types should let you do the same thing that a test would do, except exhaustively: if you add a new email address to an account with N addresses, you can then index N+1 of those addresses, but no more. The N-address account coming from the ORM isn't considered an "escape hatch" that "weakens the test system": it's just how it works. I want stronger types for exhaustive testing of business logic on individual functions -- the sort of things that a comment would say (e.g. "Returns a subset of this parameter if it is provided, otherwise..."), except machine-checked. I don't need my entire program to have a type that Messrs. Curry and Howard like. In all probability, my entire program is structured as an infinite loop anyway. I don't know that any systems really let you get here (other than maybe extraction of particular functions into Haskell or ML, but really the people who would voluntarily write their entire app in Haskell or ML are not the right target audience).

mafribe 11y ago

after a certain point the validation overhead of advanced type systems is just not worth it. But what makes you think you need dependent types to do full specification and verification of a program? Instead you could use program logic. Write the program in any language you like and later, when it the program is finished verifiy that it meets its specification using program logic. This separates programming from verification completely. In my opinion this is the future of certified programming. Dependent types are too heavyweight to support any conventional programming process. Another advantage is that unlike Curry-Howard based verification, program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This tends to yield shorter proofs. See Microsoft's Daphny [1] or CFML [2] for prototype tool chains implementing program logic based verification. Facebook's infer tool [3], while not allowing full verification, is also based on program logic. [1] http://research.microsoft.com/en-us/projects/dafny http://research.microsoft.com/en-us/projects/dafny [2] http://www.chargueraud.org/softs/cfml http://www.chargueraud.org/softs/cfml [3] https://github.com/facebook/infer https://github.com/facebook/infer

darzu 11y ago
> This separates programming from verification completely. This is simply not the case. Significant verification projects always plan for verification and do verification in tandem. This is definitely true for all Dafny projects to date as well. Verification is just so much harder than unverified programming that you generally want to do everything you can while programming to make verification easier. This may become less true as proof automation improves but it will always be a tension. > But what makes you think you need dependent types to do full specification [...] ? Also, keep in mind that Dafny and similar tools can only express first order logic; this can significantly restricts the expressiveness of your specification language and intermediate lemmas. > program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This is a silly point. First off proof assistants like Coq aren't inconsistent with the law of the excluded middle (only NuPRL is I believe) so you can always assume it as an axiom if you'd like. Most projects don't do this because constructivism is a benefit not a burden in verification: it allows you to make distinctions that aren't possible in classical logic. I agree that Dafny and similar projects are very exciting though; Dafny's tight integration with Z3 provides an awesome level of automation that will keep getting better and better.

darzu 11y ago

True certified programming has a lot of overhead but there are definitely areas where it'll be worth it: medical devices, car systems, mars rovers, aviation, etc. The University of Washington is actively working on verifying radiation therapy machine software and early results are already used in production for example. I think the reason certified programming hasn't been more widely adopted yet is because the tooling is terrible at the moment and we still have some important bits of theory to work out (e.g. homotopy type theory & other equality issues). It'll get there. Projects like Lean & Dafny at MSR, Adam Chlipala's work at MIT, and the large amount of theory work being done at CMU, Cornell, UPenn, Inria and other places are very promising. My bet is that the tooling & theory will continue to improve and eventually the overhead will become low enough that a significant portion (~10-20%) of software will be certified. I recommend reading Adam Chlipala's vision statement for inspiration on what certified programming could enable: http://adam.chlipala.net/summary.html http://adam.chlipala.net/summary.html

jules 11y ago

The reason is twofold. One, research into dependent types is still ongoing. Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Well, arguably just a single construct: it generalizes the usual function type A -> B to the dependent function type x:A -> B(x). This subsumes a lot of things like generics, existential types, GADTs, higher kinded types, rank-n polymorphism, etc. You can even use it to do record types, polymorphic variants, modules, refinement types, etc. The dependent function type is a universal lego block for types. Even more striking, it unifies the type level with the value level. Instead of having a language of types and a language of expressions there is just one language. The type List<T> takes a type T and gives you the type of lists with elements of type T. In dependently typed languages this is just a function List(T) that takes a type and returns a type. Instead of having F<T> at the type level and f(x) at the value level, there's only one kind of function that does both. I have no doubt that we will eventually be programming in a dependently typed language, the only question is when.

mafribe 11y ago
I have no doubt that we will eventually be programming in a dependently typed language, the only question is when. For the reasons I give in another posting in this thread (inability to extend dependent types beyond pure functions, and forcing the full cost of verification on early states of software productions when specifications are unstable), I predict the opposite: dependently typed verification will give way to program logic, the only question is when.
- jules 11y ago
  Why would dependent types not extend beyond pure functions? Idris has both dependent types and non pure functions, is that not satisfactory? The fact that you can write software that provably satisfies a strict specification in dependently typed languages doesn't mean that you must. It is perfectly possible to program in them like you would in a normal language. That's what I was trying to get at: dependent types are also more expressive, not just more constraining. Now that I know about dependent types I regularly run into situations where I think "gosh, if I had dependent types I wouldn't have had to put in these type casts or handle these error cases that I know for sure cannot happen". So even if you ultimately want to reason about your programs using an external program logic (which I predict we do not, but we'll see), then for expressiveness you still want your language to have dependent types for the reason I mentioned above: > Two, type system researchers promote provably correct programming as the advantage of dependent types. IMO the far more important advantage of dependent types is expressiveness and simplicity: they generalize a vast swath of different type system features and extensions to a handful of simple constructs. Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system. You can write your program as normal and later prove lemmas about functions in the program. For instance instead of saying reverse : Vec n a -> Vec n a or reverse : (xs : List a) -> {ys : List a | length xs == length ys} you can do reverse : List a -> List a and a lemma reverse_preserves_length : forall xs. length (reverse xs) == length xs It's just not the only option you have. What's this forall you say? A dependent function type of course!

lmm 11y ago

I've been doing Scala for 5+ years, real-world production code. From here it feels like the popularity of types is going up and up (and within Scala they're becoming more popular e.g. look at doobie). Haskell and OCaml look to be getting more popular, not less. Javascript is a special case because of the browser. Go is mostly displacing Python and Ruby. There's certainly no exodus of ex-Haskell programmers fleeing for less typed languages.