6 ms·

> They add significant complexity to the language and are intended to help with correctness. But are they an effective way to achieve it compared to alternative

> They add significant complexity to the language and are intended to help with correctness. But are they an effective way to achieve it compared to alternatives? Python programmers say the same about all static type systems. What alternatives do you have in mind? Are they as generally applicable as dependant types? Dependant types are a simple and unifying way to solve a variety of shortcomings with conventional statically typed systems. For example, dependant types can express first-class modules as simple records, or allow sophisticated record operations like merge to be well-typed. > [tracking algebraic effects] But is that even a worthwhile goal? Why is it nirvana to more easily do something that might not be worth doing at all? Given the various hugely expensive bugs I have been involved in (e.g. Java toString on a date reading the system locale). I would say yes. In my industry, reproducable numbers are of vital importance, so much so that the quants use Haskell in preference to something more mainstream and supported.

pron 7y ago
> Python programmers say the same about all static type systems. So what? Even if you think having X is good, that doesn't mean having 100X is necessarily better. > Dependant types are a simple and unifying way to solve a variety of shortcomings with conventional statically typed systems. But solving problems with type systems is not a business goal. Increasing correctness is. > What alternatives do you have in mind? The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods. Dependent types are a powerful, general and complex mechanism that only scales well for very simple problems. > Given the various hugely expensive bugs I have been involved in (e.g. Java toString on a date reading the system locale). I would say yes. There are easier ways, like Java's permission system, that I mentioned elsewhere.
- willtim 7y ago
  > But solving problems with type systems is not a business goal. Increasing correctness is. I gave an example of increasing correctness in the context of record data types, something almost every business app does. > The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods. And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query? > There are easier ways, like Java's permission system, that I mentioned elsewhere. Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM?
  - pron 7y ago
    > I gave an example of increasing correctness in the context of record data types, something almost every business app does. A tank is a way of getting people to work faster than walking, a concern that almost all people have, but that doesn't mean we should propose tanks for that purpose. That dependent types could increase correctness doesn't mean they should be added to a language -- unless its goal is research. This is a common problem I see. Say A is some business concern. The question we need to answer to decide whether to use solution B is not B => A but A => B. What you're saying is that if I choose to use technique X and I want to achieve Y, then this is a way to do it. This is not the same as saying this is a good technique of achieving Y. The logical implication is reversed from what we'd like to find out. At best you're saying if you use dependent types, you increase correctness. I want to know what you should do to increase correctness, and using dependent types might be the worst possible option. The question is not whether dependent types imply increased correctness, but whether wanting increased correctness implies we should use dependent types. In fact, the post cites a case study about dependent Haskell that isn't exactly a glowing review of the feature. > And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query? "Type-checking a SQL query" is not a business goal, and if I try to convert it to some goal you may have been referring to, for example, what is a good way to check if there are mistakes of some simple class in a SQL query, then I'm not sure simple testing isn't more than sufficient. Having said that, I like simple type systems, and I think they are also sufficient for that (e.g. there are typesafe SQL libraries for Java). > Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM? I don't know what the requirements are so I don't know.
- saithound 7y ago
  > The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods Model checking is great, and many tools developed by the model checking community are marvellous (especially the TLA+ model checker). But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. They scale well enough to show that that said kernel has no in-kernel storage channels that can be exploited in a side channel attack. Deductive methods scale well enough to verify (completely automaticallly, without human intervention) that the compiled binaries faithfully implement a given C program, so the compiler and linker need not be trusted. These are deep properties. You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length (not algorithm sketches or high-level system descriptions, actual code that compiles and runs). That's for deductive approaches in general. But sone of your specific claims about type theory are dubious as well. Elsewhere you claim that > The fact that even current formal verification research is mostly looking elsewhere seems to suggest that the answer is likely negative Your claim that formal methods research is mostly looking elsewhere is really stretching it. More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year. The number of submissions to ICFP's TyDe track had over 30% growth last year. TYPES already dwarfs the biggest conferences devoted to model checking or any other specific formal method. No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere". No other subfields are ezperiencing comparable growth.
  - pron 7y ago
    > But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. ... Deductive methods scale well enough to verify (completely automaticallly, without human intervention) that the compiled binaries faithfully implement a given C program, so the compiler and linker need not be trusted. Unfortunately, they do not. The two projects you mentioned are positively tiny -- they correspond to about 10KLOC of C, or less than 1/5th the size of jQuery -- and they each took world experts years of effort. Both, BTW, required serious limitations in the algorithms used to keep them simple. That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator. > You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length Concolic tests are unsound, which is why they scale so well. Model checking routinely verifies much larger codebases, so much so that people don't bothering writing papers about it. When deductive methods are used to verify a 10KLOC program that's news. You can buy off-the-shelf model checkers that do more in industry pretty much all the time. > More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year. Perhaps, but when you look at FM conferences, deductive methods in general and type systems in particular are significantly more represented. > No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere" There's no need to abandon something that has yet to break through in the first place. Most FM research is just done elsewhere. > No other subfields are ezperiencing comparable growth. Automated methods are.
- Cladode 7y ago
  better scalability than deductive This is misleading. There are two notions of scalability: - Scalable to large code bases. - Scalable to deep properties. Deductive methods are currently the only ones that scale to deep properties. Model checking et al are currently the much better at scaling to large code bases. Note however two things: First, Facebook's infer tool which scales quite well to large code bases, is partly based on deductive methods. Secondly, and most importantly, under the hood in most current approaches, SAT/SMT solvers do much of the heavy lifting. Existing SAT/SMT solvers are invariably based on DPLL, i.e. resolution, i.e. a deductive method.
  - pron 7y ago
    > Deductive methods are currently the only ones that scale to deep properties. Model checkers check deep properties with overall significantly less effort. It is true that they don't always succeed, but neither do deductive proofs. In industry, deductive methods are used as a last resort, when they're used at all, to tie together results from automated techniques. > Note however two things: ... That's not what I meant by "deductive methods;" I meant verification by semi-automated deductive proofs. Also, SMT solvers aren't used in isolation to verify significant pieces of software, they're used as components of model checkers, concolic testing and proof assistants (or to verify local properties of code units), so they're used in both semi-automated deductive methods as well as in automated methods. I also believe that DPLL is based on assignment and backtracking, not resolution.
    - Cladode 7y ago
      Model checkers check deep Which deep properties have you got in mind? DPLL is based DPLL is based on a form of resolution, in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model.
      - pron 7y ago
        > Which deep properties have you got in mind? TLC is a model checker can check most properties expressible in TLA+, which are more expressive than any base lambda-calculus theory (e.g. it includes temporal refinement properties). See my overview on TLA+'s theory: https://pron.github.io/tlaplus https://pron.github.io/tlaplus > in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model So not deductive. You know that because DPLL does not directly yield a proof of UNSAT.
- Hercuros 7y ago
  Dependent types are not just useful for proving correctness properties, and in fact I think dependent types in Haskell are not really intended to prove really complex properties, like the full functional correctness of a compiler. Hence, I think the use of Coq or Agda proofs as an example of impracticality is a strawman argument. You might need a research team and several years to show the correctness of an operating system in Coq. You do not need that to have type-safe database access or statically checked matrix sizes. Not all non-research uses of dependent types are impractical. You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever? Should Java not have added lambdas because it already had anonymous inner classes? You can clearly get by just fine in a lot of business applications without some of these features. I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness. It’s not so clear that dependent types are too complex a solution there, especially if you look at a library like Servant, which already uses some advanced type system features, and which is actually a really practical library that is probably used in production applications as well. A library like Servant might be able to expressed more clearly with dependent types than with a hodgepodge of type system extensions. I think that wanting type-safe REST API access is already an order of magnitude more practical than model checking kernel code.
  - pron 7y ago
    > Not all non-research uses of dependent types are impractical. That's like saying that a tank could get you to work, so some of its uses are practical for civilians. Does the weight of dependent types justify such disproportionate applicability? > You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever? And those arguments would be just true, except that industry languages adopted those features many years after they've been tried in research languages and shown their worth, while industry languages didn't adopt other features (or perhaps haven't yet), because they didn't prove to be the right solutions to big problems. It's perfectly fine to adopt many ideas that are open research questions, but if you do so you can't deny that your goal is research. > I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness. No, because that's the inverted implication, or "tank" problem again. Just because a tank can get you to work doesn't mean that it should. If you want to achieve goal A, and feature B achieves it, i.e. B => A, you cannot conclude from that that you should adopt B. You're assuming A and B => A and concluding B. That just doesn't follow. The question we're asking is whether A => B. We're not asking whether dependent types can be put to some practical use -- that's what researchers ask. We engineers ask what solution to our problem we should adopt (usually the least costly one).

pron 7y ago

> Python programmers say the same about all static type systems. So what? Even if you think having X is good, that doesn't mean having 100X is necessarily better. > Dependant types are a simple and unifying way to solve a variety of shortcomings with conventional statically typed systems. But solving problems with type systems is not a business goal. Increasing correctness is. > What alternatives do you have in mind? The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods. Dependent types are a powerful, general and complex mechanism that only scales well for very simple problems. > Given the various hugely expensive bugs I have been involved in (e.g. Java toString on a date reading the system locale). I would say yes. There are easier ways, like Java's permission system, that I mentioned elsewhere.

willtim 7y ago
> But solving problems with type systems is not a business goal. Increasing correctness is. I gave an example of increasing correctness in the context of record data types, something almost every business app does. > The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods. And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query? > There are easier ways, like Java's permission system, that I mentioned elsewhere. Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM?
- pron 7y ago
  > I gave an example of increasing correctness in the context of record data types, something almost every business app does. A tank is a way of getting people to work faster than walking, a concern that almost all people have, but that doesn't mean we should propose tanks for that purpose. That dependent types could increase correctness doesn't mean they should be added to a language -- unless its goal is research. This is a common problem I see. Say A is some business concern. The question we need to answer to decide whether to use solution B is not B => A but A => B. What you're saying is that if I choose to use technique X and I want to achieve Y, then this is a way to do it. This is not the same as saying this is a good technique of achieving Y. The logical implication is reversed from what we'd like to find out. At best you're saying if you use dependent types, you increase correctness. I want to know what you should do to increase correctness, and using dependent types might be the worst possible option. The question is not whether dependent types imply increased correctness, but whether wanting increased correctness implies we should use dependent types. In fact, the post cites a case study about dependent Haskell that isn't exactly a glowing review of the feature. > And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query? "Type-checking a SQL query" is not a business goal, and if I try to convert it to some goal you may have been referring to, for example, what is a good way to check if there are mistakes of some simple class in a SQL query, then I'm not sure simple testing isn't more than sufficient. Having said that, I like simple type systems, and I think they are also sufficient for that (e.g. there are typesafe SQL libraries for Java). > Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM? I don't know what the requirements are so I don't know.
saithound 7y ago
> The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods Model checking is great, and many tools developed by the model checking community are marvellous (especially the TLA+ model checker). But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. They scale well enough to show that that said kernel has no in-kernel storage channels that can be exploited in a side channel attack. Deductive methods scale well enough to verify (completely automaticallly, without human intervention) that the compiled binaries faithfully implement a given C program, so the compiler and linker need not be trusted. These are deep properties. You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length (not algorithm sketches or high-level system descriptions, actual code that compiles and runs). That's for deductive approaches in general. But sone of your specific claims about type theory are dubious as well. Elsewhere you claim that > The fact that even current formal verification research is mostly looking elsewhere seems to suggest that the answer is likely negative Your claim that formal methods research is mostly looking elsewhere is really stretching it. More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year. The number of submissions to ICFP's TyDe track had over 30% growth last year. TYPES already dwarfs the biggest conferences devoted to model checking or any other specific formal method. No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere". No other subfields are ezperiencing comparable growth.
- pron 7y ago
  > But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. ... Deductive methods scale well enough to verify (completely automaticallly, without human intervention) that the compiled binaries faithfully implement a given C program, so the compiler and linker need not be trusted. Unfortunately, they do not. The two projects you mentioned are positively tiny -- they correspond to about 10KLOC of C, or less than 1/5th the size of jQuery -- and they each took world experts years of effort. Both, BTW, required serious limitations in the algorithms used to keep them simple. That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator. > You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length Concolic tests are unsound, which is why they scale so well. Model checking routinely verifies much larger codebases, so much so that people don't bothering writing papers about it. When deductive methods are used to verify a 10KLOC program that's news. You can buy off-the-shelf model checkers that do more in industry pretty much all the time. > More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year. Perhaps, but when you look at FM conferences, deductive methods in general and type systems in particular are significantly more represented. > No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere" There's no need to abandon something that has yet to break through in the first place. Most FM research is just done elsewhere. > No other subfields are ezperiencing comparable growth. Automated methods are.
Cladode 7y ago
better scalability than deductive This is misleading. There are two notions of scalability: - Scalable to large code bases. - Scalable to deep properties. Deductive methods are currently the only ones that scale to deep properties. Model checking et al are currently the much better at scaling to large code bases. Note however two things: First, Facebook's infer tool which scales quite well to large code bases, is partly based on deductive methods. Secondly, and most importantly, under the hood in most current approaches, SAT/SMT solvers do much of the heavy lifting. Existing SAT/SMT solvers are invariably based on DPLL, i.e. resolution, i.e. a deductive method.
- pron 7y ago
  > Deductive methods are currently the only ones that scale to deep properties. Model checkers check deep properties with overall significantly less effort. It is true that they don't always succeed, but neither do deductive proofs. In industry, deductive methods are used as a last resort, when they're used at all, to tie together results from automated techniques. > Note however two things: ... That's not what I meant by "deductive methods;" I meant verification by semi-automated deductive proofs. Also, SMT solvers aren't used in isolation to verify significant pieces of software, they're used as components of model checkers, concolic testing and proof assistants (or to verify local properties of code units), so they're used in both semi-automated deductive methods as well as in automated methods. I also believe that DPLL is based on assignment and backtracking, not resolution.
  - Cladode 7y ago
    Model checkers check deep Which deep properties have you got in mind? DPLL is based DPLL is based on a form of resolution, in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model.
    - pron 7y ago
      > Which deep properties have you got in mind? TLC is a model checker can check most properties expressible in TLA+, which are more expressive than any base lambda-calculus theory (e.g. it includes temporal refinement properties). See my overview on TLA+'s theory: https://pron.github.io/tlaplus https://pron.github.io/tlaplus > in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model So not deductive. You know that because DPLL does not directly yield a proof of UNSAT.
Hercuros 7y ago
Dependent types are not just useful for proving correctness properties, and in fact I think dependent types in Haskell are not really intended to prove really complex properties, like the full functional correctness of a compiler. Hence, I think the use of Coq or Agda proofs as an example of impracticality is a strawman argument. You might need a research team and several years to show the correctness of an operating system in Coq. You do not need that to have type-safe database access or statically checked matrix sizes. Not all non-research uses of dependent types are impractical. You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever? Should Java not have added lambdas because it already had anonymous inner classes? You can clearly get by just fine in a lot of business applications without some of these features. I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness. It’s not so clear that dependent types are too complex a solution there, especially if you look at a library like Servant, which already uses some advanced type system features, and which is actually a really practical library that is probably used in production applications as well. A library like Servant might be able to expressed more clearly with dependent types than with a hodgepodge of type system extensions. I think that wanting type-safe REST API access is already an order of magnitude more practical than model checking kernel code.
- pron 7y ago
  > Not all non-research uses of dependent types are impractical. That's like saying that a tank could get you to work, so some of its uses are practical for civilians. Does the weight of dependent types justify such disproportionate applicability? > You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever? And those arguments would be just true, except that industry languages adopted those features many years after they've been tried in research languages and shown their worth, while industry languages didn't adopt other features (or perhaps haven't yet), because they didn't prove to be the right solutions to big problems. It's perfectly fine to adopt many ideas that are open research questions, but if you do so you can't deny that your goal is research. > I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness. No, because that's the inverted implication, or "tank" problem again. Just because a tank can get you to work doesn't mean that it should. If you want to achieve goal A, and feature B achieves it, i.e. B => A, you cannot conclude from that that you should adopt B. You're assuming A and B => A and concluding B. That just doesn't follow. The question we're asking is whether A => B. We're not asking whether dependent types can be put to some practical use -- that's what researchers ask. We engineers ask what solution to our problem we should adopt (usually the least costly one).