4 ms·

We aren't going to move to dependently-typed languages based around theorem proving anytime soon. The reason is simple: those languages don't support normal ind

We aren't going to move to dependently-typed languages based around theorem proving anytime soon. The reason is simple: those languages don't support normal industry development practices, where you don't have time to spend 10x the time on verification as you do on development. (They do support development practices favored by the US Department of Defense, which is perhaps part of the reason why research into such type systems attracts DARPA grants.) Where such languages may have a future is for proving some kernel of core infrastructure code correct, where the code has such a high value to size ratio that spending the time to prove it correct may cross the line into economic viability. SeL4 is a high-profile example of this. Another example that's been on my mind over the years could be proving the unsafe code in the Rust standard library correct. The latter would be interesting because it would address the criticism of "well, there's unsafe code in libstd, how can you say Rust is safe?" without burdening regular Rust users (not standard library developers) with all the baggage of a complex type system.

zozbot234 7y ago
> The reason is simple: those languages don't support normal industry development practices, where you don't have time to spend 10x the time on verification as you do on development. In practice, these languages have good support for gradual development so no, you don't have to spend 10x your dev time on verification. You can focus your verification effort on the lowest-hanging fruit, such as properties that only depend on local reasoning, as opposed to non-trivial interactions involving the program as a whole. (One potential issue for this is that dependently-typed languages are total languages, so any code that's 'natively' written in the languages must be proven to terminate. But partiality and Turing-completeness can be reintroduced in a fairly trivial way by resorting to a 'Delay' or 'Partial' monad.)
phillipcarter 7y ago
There’s also the problem where inferring the types is not decidable, so we either get slow tooling/builds or an onerous development cycle of specifying everything. The latter would be unbearable when you consider how weird and annoying things relate to one another in large, enterprisey systems.
- zozbot234 7y ago
  > There’s also the problem where inferring the types is not decidable That's a "problem" already when using some Haskell extensions. But it's only relevant in non-trivial scenarios where writing out types is not much of an extra burden.
touisteur 7y ago
Not even going to dependent types, the type system and verification capabilities of the SPARK language & toolset already allow for use in the mission-critical (and not only safety-critical) domain. The tech is progressive so you can go first for 'correct' data flow (no access to uninitialized variables, dataflow constraints like Depends, Global, very interesting stuff already), then for proof of the absence of runtime errors, then for some specific properties (think maybe properties like 'this should never happen' or properties you'd write when doing PBT) to full functional proof. On a procedure to procedure base. The progress that's been made with support of floating point is amazing. Things that were hard 3 years ago now get proved without help. Pointers are now supported via a rust-like mechanism. NVidia seems to believe in the tech (well at least for Ada) for some of its new firmwares. I've seen pure algorithmic code fully proven with similar effort as it would have taken testing /AND/ you always find bugs... People that have written some SPARK then start thinking and designing for proof. Code gets simpler, design clearer, loops more evident, added contracts help understanding the interface and clear the mind while reading code (like early returns would have done before). I don't work for AdaCore or Altran UK but I think they're amazing minds at work here.
- pcwalton 7y ago
  Maybe some folks are experimenting with it, but I would be shocked if SPARK achieves market share of 1%. Or 0.1%.
  - touisteur 7y ago
    I think it's a bootstrapping problem, similar to rust adoption. People are now getting enthusiastic about a language with lots of static guarantees and a difficult-to-please compiler, and I keep reading people almost jumping to formal proof/verification ('now that I made all this effort and I get all those static guarantees, why not go the extra static verification mile ?'. I think the rust formal-methods community should look at what's already been done with Spark2014 (Ada) and Frama-C. A large part is an adaptation of the language for proof (adding /executable/ contracts, some quantifiers, loop variants/invariants, expression functions), and another big part of the work is in why3 and all the SMT tech behind, so can be re-used 'for free'. Sure not even 0.1% market share today, and I'm not even sure Ada is above this. But it's there, it's already mature, progress is very fast, and it can be tried out for free without 'asking for a quote'. Same for Frama-C. Sure it's a paradigm shift, but it's not an academic tool with an obscure UI and no retargetable skills.
pron 7y ago
Another thing that prevents dependently-typed languages from being the future is that there are alternative verification methods that have so far shown greater promise (and receive even more grants). I think the reason for this is that some hear of those languages because they're fans of programming languages in general and maybe know something about programming language theory, and dependent types represent this discipline in formal methods research. But if you look at formal methods research more generally (e.g. read the programs of the relevant conferences), you see that this direction of dependent type systems is relatively small, and most of the research effort is focused elsewhere. I feel that some of the discussion about those languages is like an amateur runner who's thoroughly amazed by the results of an Olympic runner to the point of obsession, without knowing that they're in the seventh place. So dependently typed languages have had some achievement, but other techniques -- from CEGAR model checking to concolic testing -- have had better results, and that's why they're getting more attention in the formal methods space. The main challenge, which you alluded to, is one of scale. So far only very small programs have been verified using any semi-manual formal deductive proof methods (of which dependent type systems are one instance), and other methods have shown somewhat better scalability.
- zozbot234 7y ago
  > other techniques -- from CEGAR model checking to concolic testing -- have had better results, and that's why they're getting more attention in the formal methods space. These techniques are tailored towards efficiently finding refutations or counterexamples where a program fails correctness. They are very effective at what they do, but they're best used in combination with formal proof, or as a sort of glorified automated testing ('fuzzing').
  - pron 7y ago
    First, model checking is a proof technique, albeit in the model theory of the logic rather than in the proof theory; that it can find refutations is a major strength, though. Second, engineers build systems, and they care about the correctness of their system. This is something that cannot possibly be proven because a system is a physical object, and at best, what you can get are probabilistic guarantees (e.g. the CPU only performs the commands it is given with some probability). So what engineers want (as opposed to mathematicians or computer scientists publishing an algorithm) is a technique that most cheaply brings their system to the required correctness probability. Whether this means proving the algorithm correct or finding as many bugs as possible is completely irrelevant. So far, automated techniques like the ones I mentioned do a better job at that, and that is why they're currently considered more promising.
74ls00 7y ago
There’s not much point in providing such guarantees for most application code but there is great benefit for OS and driver code, and some benefit to most library code. Just take security. Ensuring all applications are using the latest, secure, version of a library is a hard problem and so we should do all that we can to ensure the code is correct. How valuable this exercises is depends on the size of the audience of the library
saurik 7y ago
That same argument was--and sometimes still is--made about the type system in Rust. As someone who has been building a network core recently where a small amount of dependent typing (more than I can pull off in C++, where the templating engine kind of hints in the right direction by letting you parameterize types over values) would go a long way, I personally feel like dependent typing could easily be added to existing languages, and the secret is to just make the fallback be to a runtime hard-enforced check (so it feels like something of a compiler optimization, though one where I would like to then be able to insist/check--even if only by using some external linting tool--that it is happening at compile time).

zozbot234 7y ago

> The reason is simple: those languages don't support normal industry development practices, where you don't have time to spend 10x the time on verification as you do on development. In practice, these languages have good support for gradual development so no, you don't have to spend 10x your dev time on verification. You can focus your verification effort on the lowest-hanging fruit, such as properties that only depend on local reasoning, as opposed to non-trivial interactions involving the program as a whole. (One potential issue for this is that dependently-typed languages are total languages, so any code that's 'natively' written in the languages must be proven to terminate. But partiality and Turing-completeness can be reintroduced in a fairly trivial way by resorting to a 'Delay' or 'Partial' monad.)

phillipcarter 7y ago

There’s also the problem where inferring the types is not decidable, so we either get slow tooling/builds or an onerous development cycle of specifying everything. The latter would be unbearable when you consider how weird and annoying things relate to one another in large, enterprisey systems.

zozbot234 7y ago
> There’s also the problem where inferring the types is not decidable That's a "problem" already when using some Haskell extensions. But it's only relevant in non-trivial scenarios where writing out types is not much of an extra burden.

touisteur 7y ago

Not even going to dependent types, the type system and verification capabilities of the SPARK language & toolset already allow for use in the mission-critical (and not only safety-critical) domain. The tech is progressive so you can go first for 'correct' data flow (no access to uninitialized variables, dataflow constraints like Depends, Global, very interesting stuff already), then for proof of the absence of runtime errors, then for some specific properties (think maybe properties like 'this should never happen' or properties you'd write when doing PBT) to full functional proof. On a procedure to procedure base. The progress that's been made with support of floating point is amazing. Things that were hard 3 years ago now get proved without help. Pointers are now supported via a rust-like mechanism. NVidia seems to believe in the tech (well at least for Ada) for some of its new firmwares. I've seen pure algorithmic code fully proven with similar effort as it would have taken testing /AND/ you always find bugs... People that have written some SPARK then start thinking and designing for proof. Code gets simpler, design clearer, loops more evident, added contracts help understanding the interface and clear the mind while reading code (like early returns would have done before). I don't work for AdaCore or Altran UK but I think they're amazing minds at work here.

pcwalton 7y ago
Maybe some folks are experimenting with it, but I would be shocked if SPARK achieves market share of 1%. Or 0.1%.
- touisteur 7y ago
  I think it's a bootstrapping problem, similar to rust adoption. People are now getting enthusiastic about a language with lots of static guarantees and a difficult-to-please compiler, and I keep reading people almost jumping to formal proof/verification ('now that I made all this effort and I get all those static guarantees, why not go the extra static verification mile ?'. I think the rust formal-methods community should look at what's already been done with Spark2014 (Ada) and Frama-C. A large part is an adaptation of the language for proof (adding /executable/ contracts, some quantifiers, loop variants/invariants, expression functions), and another big part of the work is in why3 and all the SMT tech behind, so can be re-used 'for free'. Sure not even 0.1% market share today, and I'm not even sure Ada is above this. But it's there, it's already mature, progress is very fast, and it can be tried out for free without 'asking for a quote'. Same for Frama-C. Sure it's a paradigm shift, but it's not an academic tool with an obscure UI and no retargetable skills.

pron 7y ago

Another thing that prevents dependently-typed languages from being the future is that there are alternative verification methods that have so far shown greater promise (and receive even more grants). I think the reason for this is that some hear of those languages because they're fans of programming languages in general and maybe know something about programming language theory, and dependent types represent this discipline in formal methods research. But if you look at formal methods research more generally (e.g. read the programs of the relevant conferences), you see that this direction of dependent type systems is relatively small, and most of the research effort is focused elsewhere. I feel that some of the discussion about those languages is like an amateur runner who's thoroughly amazed by the results of an Olympic runner to the point of obsession, without knowing that they're in the seventh place. So dependently typed languages have had some achievement, but other techniques -- from CEGAR model checking to concolic testing -- have had better results, and that's why they're getting more attention in the formal methods space. The main challenge, which you alluded to, is one of scale. So far only very small programs have been verified using any semi-manual formal deductive proof methods (of which dependent type systems are one instance), and other methods have shown somewhat better scalability.

zozbot234 7y ago
> other techniques -- from CEGAR model checking to concolic testing -- have had better results, and that's why they're getting more attention in the formal methods space. These techniques are tailored towards efficiently finding refutations or counterexamples where a program fails correctness. They are very effective at what they do, but they're best used in combination with formal proof, or as a sort of glorified automated testing ('fuzzing').
- pron 7y ago
  First, model checking is a proof technique, albeit in the model theory of the logic rather than in the proof theory; that it can find refutations is a major strength, though. Second, engineers build systems, and they care about the correctness of their system. This is something that cannot possibly be proven because a system is a physical object, and at best, what you can get are probabilistic guarantees (e.g. the CPU only performs the commands it is given with some probability). So what engineers want (as opposed to mathematicians or computer scientists publishing an algorithm) is a technique that most cheaply brings their system to the required correctness probability. Whether this means proving the algorithm correct or finding as many bugs as possible is completely irrelevant. So far, automated techniques like the ones I mentioned do a better job at that, and that is why they're currently considered more promising.

74ls00 7y ago

There’s not much point in providing such guarantees for most application code but there is great benefit for OS and driver code, and some benefit to most library code. Just take security. Ensuring all applications are using the latest, secure, version of a library is a hard problem and so we should do all that we can to ensure the code is correct. How valuable this exercises is depends on the size of the audience of the library

saurik 7y ago

That same argument was--and sometimes still is--made about the type system in Rust. As someone who has been building a network core recently where a small amount of dependent typing (more than I can pull off in C++, where the templating engine kind of hints in the right direction by letting you parameterize types over values) would go a long way, I personally feel like dependent typing could easily be added to existing languages, and the secret is to just make the fallback be to a runtime hard-enforced check (so it feels like something of a compiler optimization, though one where I would like to then be able to insist/check--even if only by using some external linting tool--that it is happening at compile time).