7 ms·

Ironically, I'd point at GHC Haskell and Scala as the prime examples of what's so wrong with programming language research today. Today's academic environment o

Ironically, I'd point at GHC Haskell and Scala as the prime examples of what's so wrong with programming language research today. Today's academic environment only rewards work that can deliver results in a short time frame, which discourages academics from doing badly needed fundamental work. What we need is “a formal semantics for a language, with practical proof principles for designing correct programs”. What academics give us is “a type system with first-class foos, with a proof of type soundness”. Pathetic.

lmm 9y ago
It's the industry that only wants small improvements that it can digest one at a time. Look at how much anti-intellectual hostility Haskell and Scala attract (even on this very site) for the really quite small steps they're taking. It's not the academics' fault.
- simon_o 9y ago
  But those language communities also have to do some self-reflection. People are often hostile to things they don't know. Not taking this into account when trying to introduce new things is a recipe for disaster. This means ... – picking up developers from where they are, not telling potential adopters "if you write Java-like Scala we don't want you here". – meaningful documentation, not answering efforts to improve documentation with "it's not necessary, because everyone already knows Scala". – describing and explaining design choices like companion objects, type classes, context bounds, and so on; not expecting that beginners will understand their superiority through osmosis. – making technologies accessible to people on their platforms, not treating backends such as Scala.js, Scala on Android or Scala-Native as add-ons for existing Scala users (or worse). – taking tooling seriously, and not releasing major versions of the language without tooling support. Or breaking compatibility in minor versions like in Scala 2.12. – clean-ups that removes unnecessary baggage from the language and its libraries. Not lecturing people about the number of keywords or counting the lines in the language's grammar in comparison to other languages. Haskell does some things better in this regard, but both are far from a convincing value proposition over "worse is better" approaches like Kotlin (which will probably swipe the floor with Scala in the future, because they address the bad parts of Scala).
  - catnaroek 9y ago
    Neither Kotlin nor any other industry language addresses my original point, namely: > What we need is “a formal semantics for a language, with practical proof principles for designing correct programs”. However, I'm not disappointed in industry languages, because I don't actually expect anything from them.
- catnaroek 9y ago
  I am not criticizing the academics behind Haskell and Scala for “not doing enough”. I am criticizing them for doing counterproductive “work”. (0) Haskell and Scala are already very complicated, and they are becoming even more complicated at a very fast rate. This will only make life harder when we finally bite the bullet and admit that we need a formal semantics for the mess we have created. (1) Moreover, this complexity only yields at best marginal increases in the extent to which these languages aid software verification. Effort would be better spent trying to figure out how much verification you can wrangle out of relatively simple type systems like ML's. I have actually tried this, and obtained (IMO) promising results: core types prove some simple things, proper use of modules proves a few more simple things, but most importantly, they make complicated things easier to (formally!) prove by other means. (2) On more philosophical grounds, the extended community behind typed functional languages draws inspiration from the wrong source. Martin-Löf type theory is doubtlessly a beautiful foundation for mathematics, but it has a fatal flaw for programming purposes: it makes no distinction between values (which are already there, you just use them) and computations (which you need to run to produce values, and might have effects during the process). As a result, a programming language based on Martin-Löf type theory has to be crippled in unacceptable ways (e.g. totality, IOW, “fixing a prior notion of acceptable recursion”) to prevent it from being type-unsound. (3) There is ample theoretical and practical evidence that no single language can be good for everything, so there will be situations in which we need to compose program fragments written in different languages. Alas, type theory is conspicuously silent about FFIs. Is this perhaps because of a refusal to acknowledge that computation is a prior notion, which types can help organize, but by no means define?
  - lmm 9y ago
    > Haskell and Scala are already very complicated, and they are becoming even more complicated at a very fast rate. This will only make life harder when we finally bite the bullet and admit that we need a formal semantics for the mess we have created. It's very hard to know what we need formal semantics for if we don't simultaneously try to write practical programs. There's a tick-tock pattern at work here: start with a clean formal language, figure out what extensions are needed to write practical programs in it, at first in an ad-hoc way, then figure out a way to make that extension in a sound, compatible way, then finally form a new clean formal language that accommodates these extensions. If you just want a language with formal semantics, ML or Haskell 98 exist already; Scala or GHC Haskell extend these to languages we can write industrial programs with, and then Dotty or Idris are clean formalisable designs with the lessons learned from this. > Moreover, this complexity only yields at best marginal increases in the extent to which these languages aid software verification. Effort would be better spent trying to figure out how much verification you can wrangle out of relatively simple type systems like ML's. I have actually tried this, and obtained (IMO) promising results: core types prove some simple things, proper use of modules proves a few more simple things, but most importantly, they make complicated things easier to (formally!) prove by other means. Not my experience. I've found HKT and dependent types extremely useful in practice; they give me a simple way to directly encode the business properties I care about verifying. Of course if you've come up with something useful I'm interested, and I'm sure many others would be, but I'd strongly disagree with the notion that what the academics are doing isn't useful. > As a result, a programming language based on Martin-Löf type theory has to be crippled in unacceptable ways (e.g. totality, IOW, “fixing a prior notion of acceptable recursion”) to prevent it from being type-unsound. Not at all convinced that e.g. Idris-style totality is "unacceptable". What's the problem with it? > There is ample theoretical and practical evidence that no single language can be good for everything, so there will be situations in which we need to compose program fragments written in different languages. Again not at all convinced. Certainly my practical Scala experience is that it's good for everything.

lmm 9y ago

It's the industry that only wants small improvements that it can digest one at a time. Look at how much anti-intellectual hostility Haskell and Scala attract (even on this very site) for the really quite small steps they're taking. It's not the academics' fault.

simon_o 9y ago
But those language communities also have to do some self-reflection. People are often hostile to things they don't know. Not taking this into account when trying to introduce new things is a recipe for disaster. This means ... – picking up developers from where they are, not telling potential adopters "if you write Java-like Scala we don't want you here". – meaningful documentation, not answering efforts to improve documentation with "it's not necessary, because everyone already knows Scala". – describing and explaining design choices like companion objects, type classes, context bounds, and so on; not expecting that beginners will understand their superiority through osmosis. – making technologies accessible to people on their platforms, not treating backends such as Scala.js, Scala on Android or Scala-Native as add-ons for existing Scala users (or worse). – taking tooling seriously, and not releasing major versions of the language without tooling support. Or breaking compatibility in minor versions like in Scala 2.12. – clean-ups that removes unnecessary baggage from the language and its libraries. Not lecturing people about the number of keywords or counting the lines in the language's grammar in comparison to other languages. Haskell does some things better in this regard, but both are far from a convincing value proposition over "worse is better" approaches like Kotlin (which will probably swipe the floor with Scala in the future, because they address the bad parts of Scala).
- catnaroek 9y ago
  Neither Kotlin nor any other industry language addresses my original point, namely: > What we need is “a formal semantics for a language, with practical proof principles for designing correct programs”. However, I'm not disappointed in industry languages, because I don't actually expect anything from them.
catnaroek 9y ago
I am not criticizing the academics behind Haskell and Scala for “not doing enough”. I am criticizing them for doing counterproductive “work”. (0) Haskell and Scala are already very complicated, and they are becoming even more complicated at a very fast rate. This will only make life harder when we finally bite the bullet and admit that we need a formal semantics for the mess we have created. (1) Moreover, this complexity only yields at best marginal increases in the extent to which these languages aid software verification. Effort would be better spent trying to figure out how much verification you can wrangle out of relatively simple type systems like ML's. I have actually tried this, and obtained (IMO) promising results: core types prove some simple things, proper use of modules proves a few more simple things, but most importantly, they make complicated things easier to (formally!) prove by other means. (2) On more philosophical grounds, the extended community behind typed functional languages draws inspiration from the wrong source. Martin-Löf type theory is doubtlessly a beautiful foundation for mathematics, but it has a fatal flaw for programming purposes: it makes no distinction between values (which are already there, you just use them) and computations (which you need to run to produce values, and might have effects during the process). As a result, a programming language based on Martin-Löf type theory has to be crippled in unacceptable ways (e.g. totality, IOW, “fixing a prior notion of acceptable recursion”) to prevent it from being type-unsound. (3) There is ample theoretical and practical evidence that no single language can be good for everything, so there will be situations in which we need to compose program fragments written in different languages. Alas, type theory is conspicuously silent about FFIs. Is this perhaps because of a refusal to acknowledge that computation is a prior notion, which types can help organize, but by no means define?
- lmm 9y ago
  > Haskell and Scala are already very complicated, and they are becoming even more complicated at a very fast rate. This will only make life harder when we finally bite the bullet and admit that we need a formal semantics for the mess we have created. It's very hard to know what we need formal semantics for if we don't simultaneously try to write practical programs. There's a tick-tock pattern at work here: start with a clean formal language, figure out what extensions are needed to write practical programs in it, at first in an ad-hoc way, then figure out a way to make that extension in a sound, compatible way, then finally form a new clean formal language that accommodates these extensions. If you just want a language with formal semantics, ML or Haskell 98 exist already; Scala or GHC Haskell extend these to languages we can write industrial programs with, and then Dotty or Idris are clean formalisable designs with the lessons learned from this. > Moreover, this complexity only yields at best marginal increases in the extent to which these languages aid software verification. Effort would be better spent trying to figure out how much verification you can wrangle out of relatively simple type systems like ML's. I have actually tried this, and obtained (IMO) promising results: core types prove some simple things, proper use of modules proves a few more simple things, but most importantly, they make complicated things easier to (formally!) prove by other means. Not my experience. I've found HKT and dependent types extremely useful in practice; they give me a simple way to directly encode the business properties I care about verifying. Of course if you've come up with something useful I'm interested, and I'm sure many others would be, but I'd strongly disagree with the notion that what the academics are doing isn't useful. > As a result, a programming language based on Martin-Löf type theory has to be crippled in unacceptable ways (e.g. totality, IOW, “fixing a prior notion of acceptable recursion”) to prevent it from being type-unsound. Not at all convinced that e.g. Idris-style totality is "unacceptable". What's the problem with it? > There is ample theoretical and practical evidence that no single language can be good for everything, so there will be situations in which we need to compose program fragments written in different languages. Again not at all convinced. Certainly my practical Scala experience is that it's good for everything.