4 ms·

Because imperative programming is not very interesting from a programming language theory point of view. If this was a list about compiler construction, it woul

by exDM69 11y ago

Because imperative programming is not very interesting from a programming language theory point of view. If this was a list about compiler construction, it would look very different. As we're seeing more and more language features originating from functional programming trickle into mainstream languages, this research hasn't clearly gone to waste even though everyone is not programming in functional programming languages.

mafribe 11y ago
imperative programming is not very interesting from a programming language theory point of view. I'm afraid I disagree, the opposite is the case. Modern PL theory is mostly about program correctness, and that is much easier for pure functional languages. Until recently, nobody had a handle on program logics for imperative languages, or reasoning techniques for operational semantics. The only available reasoning techniques used to be based on denotational semantics, following Scott's breakthrough domain-theoretic semantics of lambda-calculus. That's why so much theory was developed in a functional programming context, because FP is in some ways much simpler than imperative or concurrent programming (even though compiling FP languages is harder). The available textbooks reflect this state of afairs. All that has changed in the last decade or so, but it will take another decade or so before recent research insights into non-functional languages perlocates down to accessible textbooks.
- habitue 11y ago
  This is the real answer. The restrictions on functional languages that make them (perhaps) harder to use for everyday programming makes them much easier to reason about and prove properties of.
- exDM69 11y ago
  Oh, I agree with this. "Interesting" was a poor choice of words. It's definitely interesting but then again, as you say this changed in the past decade or so. Getting introduced to a new topic by exploring the latest state of the art without going through the basic theory first isn't a good way to learn most subjects.
- xjia 11y ago
  If program correctness is easy to prove, why we are not doing that when using either C or Haskell?
  - sgeisenh 11y ago
    Check out compcert for a verified c compiler. And several Haskell projects have been verified.
    - xjia 11y ago
      I know it is possible. But I wonder what stops us from doing it for most programs we write from day to day. And, if proving correctness is indeed important (I believe so), can we do something / what is the next thing to do to enable us proving correctness in our daily job.
      - mafribe 11y ago
        What stops us is cost. Formally verifying non-trivial properties (in the sense of CompCert) with current technology is several orders of magnitude more expensive and time-consuming than programming and a bit of testing. And this price is almost never worth it. We hope that this cost can be lowered in the future.
      - sgeisenh 11y ago
        The commonplace languages in use are difficult to reason about. It would take a serious paradigm shift for most companies to stop what they're doing and develop a tool chain for wholesale program verification. Additionally, it takes a special breed of programmer to be able and willing to write code in such a way that enables verification, then actually take the time to verify it. Functional programming is a jump for most main stream engineers, it is an altogether different matter to recruit or develop a team of engineers familiar with dependent type theory and formal verification. The industry tends to lag behind academia by at least a couple decades. In the 90's, lots of research was being devoted to functional programming and the various applications of type systems. Now we see various companies starting to use languages like Haskell and ocaml. Nowadays, it seems like dependent types and program verification are popular in academia, so maybe we'll see some of that by 2030.
vezzy-fnord 11y ago
Because imperative programming is not very interesting from a programming language theory point of view. I don't know, I find GCL and predicate transformer semantics to be quite interesting. Esterel's approach to synchronous reactive systems, too. I don't see why the research potential in imperative languages couldn't be ripe. The semantic possibilities are large. A ton of PL and OS research from ETH Zurich, Xerox PARC and Bell Labs alike have been from imperative language designs.

by exDM69 11y ago

mafribe 11y ago

imperative programming is not very interesting from a programming language theory point of view. I'm afraid I disagree, the opposite is the case. Modern PL theory is mostly about program correctness, and that is much easier for pure functional languages. Until recently, nobody had a handle on program logics for imperative languages, or reasoning techniques for operational semantics. The only available reasoning techniques used to be based on denotational semantics, following Scott's breakthrough domain-theoretic semantics of lambda-calculus. That's why so much theory was developed in a functional programming context, because FP is in some ways much simpler than imperative or concurrent programming (even though compiling FP languages is harder). The available textbooks reflect this state of afairs. All that has changed in the last decade or so, but it will take another decade or so before recent research insights into non-functional languages perlocates down to accessible textbooks.

habitue 11y ago
This is the real answer. The restrictions on functional languages that make them (perhaps) harder to use for everyday programming makes them much easier to reason about and prove properties of.
exDM69 11y ago
Oh, I agree with this. "Interesting" was a poor choice of words. It's definitely interesting but then again, as you say this changed in the past decade or so. Getting introduced to a new topic by exploring the latest state of the art without going through the basic theory first isn't a good way to learn most subjects.
xjia 11y ago
If program correctness is easy to prove, why we are not doing that when using either C or Haskell?
- sgeisenh 11y ago
  Check out compcert for a verified c compiler. And several Haskell projects have been verified.
  - xjia 11y ago
    I know it is possible. But I wonder what stops us from doing it for most programs we write from day to day. And, if proving correctness is indeed important (I believe so), can we do something / what is the next thing to do to enable us proving correctness in our daily job.
    - mafribe 11y ago
      What stops us is cost. Formally verifying non-trivial properties (in the sense of CompCert) with current technology is several orders of magnitude more expensive and time-consuming than programming and a bit of testing. And this price is almost never worth it. We hope that this cost can be lowered in the future.
    - sgeisenh 11y ago
      The commonplace languages in use are difficult to reason about. It would take a serious paradigm shift for most companies to stop what they're doing and develop a tool chain for wholesale program verification. Additionally, it takes a special breed of programmer to be able and willing to write code in such a way that enables verification, then actually take the time to verify it. Functional programming is a jump for most main stream engineers, it is an altogether different matter to recruit or develop a team of engineers familiar with dependent type theory and formal verification. The industry tends to lag behind academia by at least a couple decades. In the 90's, lots of research was being devoted to functional programming and the various applications of type systems. Now we see various companies starting to use languages like Haskell and ocaml. Nowadays, it seems like dependent types and program verification are popular in academia, so maybe we'll see some of that by 2030.

vezzy-fnord 11y ago

Because imperative programming is not very interesting from a programming language theory point of view. I don't know, I find GCL and predicate transformer semantics to be quite interesting. Esterel's approach to synchronous reactive systems, too. I don't see why the research potential in imperative languages couldn't be ripe. The semantic possibilities are large. A ton of PL and OS research from ETH Zurich, Xerox PARC and Bell Labs alike have been from imperative language designs.