3 ms·

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

by 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.
- stingraycharles 11y ago
  I think this is exactly what's happening, but through the back door: rather than everyone switching to Haskell, you see features pioneered by languages like Haskell being implemented in more mainstream languages. Also, do not forget Haskell's roots were to create a programming language environment where people studying compilers could easily experiment with new features. Hence Haskell's large number of language extensions.
  - theseoafs 11y ago
    Right. What I'm saying is: how long do these dependently typed language features have to "incubate" before they make it into Java? Because implementations of dependently typed languages have existed for as long as Haskell has, and we've known that it's been possible to capture "proofs" in a type system for almost a century. So how much longer do you expect it will take? Or, maybe, there just isn't a real industry demand for dependent types. Hell, many engineers still have trouble convincing their employers to write robust tests, let alone full proofs of correctness.

by Drup 11y ago

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.
stingraycharles 11y ago
I think this is exactly what's happening, but through the back door: rather than everyone switching to Haskell, you see features pioneered by languages like Haskell being implemented in more mainstream languages. Also, do not forget Haskell's roots were to create a programming language environment where people studying compilers could easily experiment with new features. Hence Haskell's large number of language extensions.
- theseoafs 11y ago
  Right. What I'm saying is: how long do these dependently typed language features have to "incubate" before they make it into Java? Because implementations of dependently typed languages have existed for as long as Haskell has, and we've known that it's been possible to capture "proofs" in a type system for almost a century. So how much longer do you expect it will take? Or, maybe, there just isn't a real industry demand for dependent types. Hell, many engineers still have trouble convincing their employers to write robust tests, let alone full proofs of correctness.