3 ms·

I like this because it addresses part of the problem of why I've stopped paying any attention to PLT related topics like denotational semantics, monads, categor

I like this because it addresses part of the problem of why I've stopped paying any attention to PLT related topics like denotational semantics, monads, category theory, and higher-order/dependent static type systems in general. In my day to day work the programming language is never the problem because hacking around the limitations of the language to bridge the gap between the problem domain and the computational domain is never the bottleneck. The real problem is when these systems go into production and all static guarantees and beautiful abstractions become basically useless. What I want is something to help me reason about dynamic and evolving large scale software systems. What I get is PLT researchers and library authors bickering over dependent types, monads, and continuations. Here's a concrete and unsolved problem. How do you specify some kind of topology for your production environment and then have whatever system understands this specification reason about performance, error recovery, failover, and scaling issues. In fact the lower level components don't even matter because you could write it in Haskell or Python or Java or whatever is your favorite language. Right now there is nothing because everyone is arguing about continuations and monads. Basically everyone involved is thinking too small. The one person that I think comes close to approaching the problem from the right angle is http://www.cl.cam.ac.uk/~srk31/ http://www.cl.cam.ac.uk/~srk31/.

zoul 11y ago
Doesn’t an expressive and strong type system, as an example, help you reason about software systems?
- dkarapetyan 11y ago
  Nope, my problem isn't reasoning about the lower level components. In fact you can assume I have correctness proofs for every piece of the infrastructure. What I don't have is the higher-level piece that can reason about the lower level components and do so when new pieces are added, old pieces removed, new guarantees enforced, old ones relaxed, etc. A static type system no matter how advanced doesn't help with any of it.
  - pron 11y ago
    Yep, that's called the "halting problem", and I hear it's very hard to solve :) Here's how I generally see it. Writing large software is hard (and a software composed of multiple components is large software, even if you decide using the network stack when calling some functions is a good idea ;)). "Type" people (and I'm certainly for some kinds of static types, I just don't think that they're the solution to everything) would tell you that types help restrict your computation in such a way that reasoning about it is easier. To that I say, but I want to do something specific which it's pretty annoying in PFP, and they answer, just do it a different way, to which I say, if I can do it differently, so can the compiler on my behalf. In short, I don't think that explicit types (i.e. those that can be defined in the language you use) are stronger than implicit types (i.e. anything that a verifier can prove about your program), and at least in theory, they are both "the same" (though, see another comment here on what I think about two things being the same in a mathematical sense). We should use whatever is easier for our minds to grasp. The more essential problem -- although I don't know if it's more interesting or less interesting -- is what exactly do we want to do in our programs? If we require a Turing complete model, then no matter how many types -- explicit or implicit -- we throw at the problem, we just won't be able to formally prove properties we might care about. Some people, however, claim that we don't really need Turing completeness, and if we don't, that might open a whole new world of possibilities. But once we start restricting the computational model, the representation we use -- say, PFP or imperative -- might become much more important, each being able to compute things that the other cannot (we know that lambda calculus and Turing machines both compute the same functions, but once we restrict each in some arbitrary ways, it gets harder to find equivalences between restrictions in the PFP model and those in the imperative model). Finally, I think that the notions of what it means "to reason about" or even what it means to be correct (and certainly how important it is to be correct) are themselves vague and require answers from empirical psychological/sociological/economic research than from math.
    - dkarapetyan 11y ago
      I think the people that say we don't need Turing completeness say that because their models can't really accommodate proper reasoning about exactly the kinds of systems I want to reason about. Proving theorems is nice and all but at the end of the day the temporal and dynamic aspects of the system I'm building are what I really care about. Not some static snapshot of it but the actual evolving gestalt.

zoul 11y ago

Doesn’t an expressive and strong type system, as an example, help you reason about software systems?

dkarapetyan 11y ago
Nope, my problem isn't reasoning about the lower level components. In fact you can assume I have correctness proofs for every piece of the infrastructure. What I don't have is the higher-level piece that can reason about the lower level components and do so when new pieces are added, old pieces removed, new guarantees enforced, old ones relaxed, etc. A static type system no matter how advanced doesn't help with any of it.
- pron 11y ago
  Yep, that's called the "halting problem", and I hear it's very hard to solve :) Here's how I generally see it. Writing large software is hard (and a software composed of multiple components is large software, even if you decide using the network stack when calling some functions is a good idea ;)). "Type" people (and I'm certainly for some kinds of static types, I just don't think that they're the solution to everything) would tell you that types help restrict your computation in such a way that reasoning about it is easier. To that I say, but I want to do something specific which it's pretty annoying in PFP, and they answer, just do it a different way, to which I say, if I can do it differently, so can the compiler on my behalf. In short, I don't think that explicit types (i.e. those that can be defined in the language you use) are stronger than implicit types (i.e. anything that a verifier can prove about your program), and at least in theory, they are both "the same" (though, see another comment here on what I think about two things being the same in a mathematical sense). We should use whatever is easier for our minds to grasp. The more essential problem -- although I don't know if it's more interesting or less interesting -- is what exactly do we want to do in our programs? If we require a Turing complete model, then no matter how many types -- explicit or implicit -- we throw at the problem, we just won't be able to formally prove properties we might care about. Some people, however, claim that we don't really need Turing completeness, and if we don't, that might open a whole new world of possibilities. But once we start restricting the computational model, the representation we use -- say, PFP or imperative -- might become much more important, each being able to compute things that the other cannot (we know that lambda calculus and Turing machines both compute the same functions, but once we restrict each in some arbitrary ways, it gets harder to find equivalences between restrictions in the PFP model and those in the imperative model). Finally, I think that the notions of what it means "to reason about" or even what it means to be correct (and certainly how important it is to be correct) are themselves vague and require answers from empirical psychological/sociological/economic research than from math.
  - dkarapetyan 11y ago
    I think the people that say we don't need Turing completeness say that because their models can't really accommodate proper reasoning about exactly the kinds of systems I want to reason about. Proving theorems is nice and all but at the end of the day the temporal and dynamic aspects of the system I'm building are what I really care about. Not some static snapshot of it but the actual evolving gestalt.