2. Oracle problem: In practise you never have full specifications (let me be
provocative: Facebook has no specification in principle, only its ever changing code), and often,
especially in early phases you rarely have specifications.
3. You pay the price for dependent types always (e.g. having to prove
termination), even if you don't use interesting specifications.
4. Like Java's exception specifications, dependent types are 'non
local', meaning that a change in one part of the code may ripple
through the entire code bases, this stands in the way of quick code
evolution, which is important -- at least in early parts of
large-scale software projects.
5. Despite dependent types being 1/2 century old by now, and despite intensive effort, dependent
types have not really been successfully been generalised to other
forms of computing (OO, stateful, concurrecy, parallel, distributed,
timed) -- unlike competing approaches.
Summary: dependent types are wonderful as a foundations of
mathematics, but have failed to live up to their promise as general
purpose languages.
1. Bidirectional typing can be easily generalized to dependent types. You can't always infer the type, but an 80% solution is definitely good enough for inference.
2. Your types don't have to be full specifications, and you can refine them later, no?
3. Idris, at least, doesn't force you to make all your functions total, and functions are actually partial by default.
4. Again, in Idris, implementations are hidden by default across modules. Maybe there's a nice middle-ground between hiding everything and exposing everything, but I don't know what that would look like.
5. What are the competing approaches and how are they better at dealing with, for example, distributed computing?
I'm not very familiar with dependent types, but none of these seem like fundamental restrictions.
Every single one of your claims is addressed by the programming language Idris [1], which has dependent types. This is not to say that Idris is the only dependently typed language which solves these issues, only that it exists as a counterexample to your claims.
1. Idris does not have type inference at the top level, but it does infer types within the body of functions. It can even disambiguate identically-named functions with different types, something Haskell cannot do.
Moreover, Idris (and other dependently typed languages) can perform implementation inference, something which is much more powerful and useful to the programmer than type inference. It lets you work interactively with the Idris compiler whereby you specify a type and Idris creates a skeleton of the function for you, filled with holes that you replace with expressions. You can ask Idris what the type of a hole is and it will helpfully tell you the types of all other identifiers in scope. You can even ask Idris to attempt to fill in the hole for you, something it can usually do when there is only one possible expression with that type (occurs extremely often in practice).
Watch Edwin Brady's demo of Idris 2 [2] to see this form of interactive development in action. Note that although Idris 2 isn't finished yet, a great deal of these examples (such as zip) work in Idris 1.3.2 (the current release).
2. Idris lets you specify your program gradually. When problems arise, you can refine your types and Idris will guide you through all of the refactoring you need to do to enforce your new invariants.
3. Idris does not force all of your functions to be total, only the ones you want to use in types. Idris checks the totality of all your functions and can produce compilation errors based on totality annotations attached to your functions. In practice, It is not very hard to make every function in your program total, apart from the main loop.
4. Idris has modules and gives you powerful tools (such as views) that allow you to define a stable API at the module boundary. This means you can mess around with any of the types of private functions to your heart's content, without any visible change to the outside world. This is entirely the opposite of 'non local' Java exceptions.
5. Idris has extremely powerful tools for working with state and writing concurrent programs which preserve invariants that cannot otherwise be checked easily with other tools. As for OO, well, that's a concept so nebulous as to be almost incoherent at this point. In practice, Idris's interfaces can dispatch on as many parameters as you want, unlike most OO languages which only do single dispatch.
1. Problems with type inference is a problem introduced with polymorphism with implicit type variables and isn't exclusive to dependent types, 'f = show . read' shouldn't compile because of type ambiguity. What is so specific about dependent types in this regard?
1. Dependent types, because they offer 100% certainty in the propositions they express (assuming they're proven) suffer from the same problem all sound verification methods suffer from, and that is fundamental computational complexity costs of verifying something with absolute certainty. I summarized some of them here: https://pron.github.io/posts/correctness-and-complexity (there are some properties that are easy to verify called inductive or compositional properties -- not surprisingly, the properties verified by simple type systems or Rust's borrow checker fall in that category -- but, unfortunately, most correctness properties aren't compositional).
2. Dependent types rely on deductive proofs for verification, and deductive proofs (the "proof theory" part of a logic) are the least scalable verification method as they are least amenable to automation. That's why model checkers (that provide proofs based on the "model theory" of the logic, hence the name model checkers) scale to larger programs/specifications. In addition, deductive proofs are much less forgiving of partial specifications. In other words, the contract (or type, in the case of dependent types) must express every property of the algorithm you rely on (unlike, say, concolic testing). This makes writing specifications very tedious. Unsurprisingly, deductive proofs are the least used formal verification technique in industry, and it's usually used when all other options have failed or to tie together results obtained from model checkers.
Those were the theoretical limitations. Here are the practical ones:
3. Unlike contracts, type systems tie the specification method (types) to the verification method (type-checking, i.e. deductive proofs). This means that everything specified with a dependent type must be deductively proven, or it has to be specified in some other way (i.e. you also need contracts), or else you risk making even your simple types unsound (although I hear some people are working on relaxing that problem, and that's what I mentioned in my previous comment). But properties differ greatly both in the confidence you need as well as the effort they require to achieve that confidence. Contracts give you the freedom to specify your program however you like, and then choose, for each property, which method you'd like to use to verify it -- deductive proofs, model checking, static analysis, concolic tests. randomized tests, manual tests or even inspection, all without risking the soundness of the type system, on which the compiler relies to generate correct machine code. In short: dependent types are inflexible in that they force you to use a particular verification method, and that verification method happens to be the least scalable, most tedious one.
4. Because dependent types are so tied to the program, the program must be written with the specific properties you want to verify in mind. If, after writing the program, you want to prove other properties about it, you'll probably need to rewrite it.
I don't think human programmers have any hope of ever being able to maintain noncompositional program properties for nontrivial programs. A model checker may indeed be able to prove some program property without the programmer having to understand why or how that property holds (in contrast to using dependent types) - but I submit that this is not actually much of an advantage; a human working on the codebase will still need a deductive-proof-like understanding.
> This means that everything specified with a dependent type must be deductively proven, or it has to be specified in some other way (i.e. you also need contracts), or else you risk making even your simple types unsound (although I hear some people are working on relaxing that problem, and that's what I mentioned in my previous comment). But properties differ greatly both in the confidence you need as well as the effort they require to achieve that confidence. Contracts give you the freedom to specify your program however you like, and then choose, for each property, which method you'd like to use to verify it -- deductive proofs, model checking, static analysis, concolic tests.
What practical distinction are you drawing here? Surely with any approach you either have a fully sound proof of a given proposition, or you have a potentially unsound proposition that you've tested at whatever level you feel appropriate. Like, if I have a SortedList type that can produce an assertion that, given n <= m, l[n] <= l[m], either the constructors of SortedList bake that in as a deductive proof, or they unsoundly assert it and I apply some level of static analysis and/or testing to them - how's that any different from what I'd do using any other technique?
> 4. Because dependent types are so tied to the program, the program must be written with the specific properties you want to verify in mind. If, after writing the program, you want to prove other properties about it, you'll probably need to rewrite it.
I'm not entirely convinced that this is any harder than any other approach - you'd have to propagate the new properties you were interested in through the code, sure, which would likely involve changing the types that the relevant points in the program were annotated with. But isn't it much the same process with a detached proof of the program property?
First of all, I would agree with you that full formalization of program correctness using dependent types is generally extremely costly in terms of time and money, and that there are often other formal methods which might get you results that are "good enough" while requiring much less effort and expertise. However, I do think that there are some inaccuracies in some of the statements you are making about proof assistants based on dependent types.
One major benefit that proof assistants have over other formal methods is that they can be used to prove essentially arbitrary properties of programs, which is not true of any automated methods. Basically, if we as humans are able to convince ourselves that a program has a certain property, then we could also show this using a (dependently-typed) proof assistant.
(Yes, theoretically all proof systems have limitations due to Gödel’s incompleteness theorem, but this limitation applies just the same to ALL formal methods. Furthermore, you’re not that likely to run into it in practice unless you are doing metatheory, and even there many interesting statements CAN still be shown.)
Consider the formally verified C compiler CompCert, where the assembly output of the compiler has been proven to have the same behavior as the input source code. A proof like this simply cannot be done using automated methods currently, and requires human assistance. This kind of correctness proof is also highly non-compositional, since the correctness proof of a compiler does not mirror the structure of the compiler very closely. Hence this also invalidates your point about dependent types not being able to handle non-compositional properties very well. There are plenty of other examples, like the seL4 microkernel.
I also do not understand what bearing computational complexity results have on humans manually formalizing their informal intuitions about program correctness in a proof assistant. Humans do not work on arbitrary problems where they have no intuition at all about why a program is correct, hence referring to worst-case computational complexity results does not make much sense here. In fact, if you have no intuition about why a program works, then how did you manage to write it in the first place? You surely did not write random garbage in the hopes that you would get a working program.
You might say that there are programs you can check using a model checker, but which humans cannot reasonably keep in their heads or form an intuition about, and therefore these proofs cannot formalized in a proof assistant. But what you can do is implement a model checker in your proof assistant and then show that the model checker is correct. After you've done that, you can simply use the model checker to do your proofs for you. And of course it should be possible to formalize the model checker itself, since the people that wrote the model checker must have some intuition about why it works and produces the correct results.
In this sense, proof assistants subsume all other formal methods, since they can be "scripted" to include them.
Furthermore, it is generally not the case that you have to rewrite your program in case you want to prove some more properties about it. You may be thinking of a programming style where the type of a program encodes all the properties you are interested in, but you can avoid this style where necessary, by separating your program and its correctness proof.
9q9|6 years ago
2. Oracle problem: In practise you never have full specifications (let me be provocative: Facebook has no specification in principle, only its ever changing code), and often, especially in early phases you rarely have specifications.
3. You pay the price for dependent types always (e.g. having to prove termination), even if you don't use interesting specifications.
4. Like Java's exception specifications, dependent types are 'non local', meaning that a change in one part of the code may ripple through the entire code bases, this stands in the way of quick code evolution, which is important -- at least in early parts of large-scale software projects.
5. Despite dependent types being 1/2 century old by now, and despite intensive effort, dependent types have not really been successfully been generalised to other forms of computing (OO, stateful, concurrecy, parallel, distributed, timed) -- unlike competing approaches.
Summary: dependent types are wonderful as a foundations of mathematics, but have failed to live up to their promise as general purpose languages.
hope-striker|6 years ago
2. Your types don't have to be full specifications, and you can refine them later, no?
3. Idris, at least, doesn't force you to make all your functions total, and functions are actually partial by default.
4. Again, in Idris, implementations are hidden by default across modules. Maybe there's a nice middle-ground between hiding everything and exposing everything, but I don't know what that would look like.
5. What are the competing approaches and how are they better at dealing with, for example, distributed computing?
I'm not very familiar with dependent types, but none of these seem like fundamental restrictions.
chongli|6 years ago
1. Idris does not have type inference at the top level, but it does infer types within the body of functions. It can even disambiguate identically-named functions with different types, something Haskell cannot do.
Moreover, Idris (and other dependently typed languages) can perform implementation inference, something which is much more powerful and useful to the programmer than type inference. It lets you work interactively with the Idris compiler whereby you specify a type and Idris creates a skeleton of the function for you, filled with holes that you replace with expressions. You can ask Idris what the type of a hole is and it will helpfully tell you the types of all other identifiers in scope. You can even ask Idris to attempt to fill in the hole for you, something it can usually do when there is only one possible expression with that type (occurs extremely often in practice).
Watch Edwin Brady's demo of Idris 2 [2] to see this form of interactive development in action. Note that although Idris 2 isn't finished yet, a great deal of these examples (such as zip) work in Idris 1.3.2 (the current release).
2. Idris lets you specify your program gradually. When problems arise, you can refine your types and Idris will guide you through all of the refactoring you need to do to enforce your new invariants.
3. Idris does not force all of your functions to be total, only the ones you want to use in types. Idris checks the totality of all your functions and can produce compilation errors based on totality annotations attached to your functions. In practice, It is not very hard to make every function in your program total, apart from the main loop.
4. Idris has modules and gives you powerful tools (such as views) that allow you to define a stable API at the module boundary. This means you can mess around with any of the types of private functions to your heart's content, without any visible change to the outside world. This is entirely the opposite of 'non local' Java exceptions.
5. Idris has extremely powerful tools for working with state and writing concurrent programs which preserve invariants that cannot otherwise be checked easily with other tools. As for OO, well, that's a concept so nebulous as to be almost incoherent at this point. In practice, Idris's interfaces can dispatch on as many parameters as you want, unlike most OO languages which only do single dispatch.
[1] https://www.idris-lang.org
[2] https://www.youtube.com/watch?v=DRq2NgeFcO0
permeakra|6 years ago
pron|6 years ago
1. Dependent types, because they offer 100% certainty in the propositions they express (assuming they're proven) suffer from the same problem all sound verification methods suffer from, and that is fundamental computational complexity costs of verifying something with absolute certainty. I summarized some of them here: https://pron.github.io/posts/correctness-and-complexity (there are some properties that are easy to verify called inductive or compositional properties -- not surprisingly, the properties verified by simple type systems or Rust's borrow checker fall in that category -- but, unfortunately, most correctness properties aren't compositional).
2. Dependent types rely on deductive proofs for verification, and deductive proofs (the "proof theory" part of a logic) are the least scalable verification method as they are least amenable to automation. That's why model checkers (that provide proofs based on the "model theory" of the logic, hence the name model checkers) scale to larger programs/specifications. In addition, deductive proofs are much less forgiving of partial specifications. In other words, the contract (or type, in the case of dependent types) must express every property of the algorithm you rely on (unlike, say, concolic testing). This makes writing specifications very tedious. Unsurprisingly, deductive proofs are the least used formal verification technique in industry, and it's usually used when all other options have failed or to tie together results obtained from model checkers.
Those were the theoretical limitations. Here are the practical ones:
3. Unlike contracts, type systems tie the specification method (types) to the verification method (type-checking, i.e. deductive proofs). This means that everything specified with a dependent type must be deductively proven, or it has to be specified in some other way (i.e. you also need contracts), or else you risk making even your simple types unsound (although I hear some people are working on relaxing that problem, and that's what I mentioned in my previous comment). But properties differ greatly both in the confidence you need as well as the effort they require to achieve that confidence. Contracts give you the freedom to specify your program however you like, and then choose, for each property, which method you'd like to use to verify it -- deductive proofs, model checking, static analysis, concolic tests. randomized tests, manual tests or even inspection, all without risking the soundness of the type system, on which the compiler relies to generate correct machine code. In short: dependent types are inflexible in that they force you to use a particular verification method, and that verification method happens to be the least scalable, most tedious one.
4. Because dependent types are so tied to the program, the program must be written with the specific properties you want to verify in mind. If, after writing the program, you want to prove other properties about it, you'll probably need to rewrite it.
lmm|6 years ago
> This means that everything specified with a dependent type must be deductively proven, or it has to be specified in some other way (i.e. you also need contracts), or else you risk making even your simple types unsound (although I hear some people are working on relaxing that problem, and that's what I mentioned in my previous comment). But properties differ greatly both in the confidence you need as well as the effort they require to achieve that confidence. Contracts give you the freedom to specify your program however you like, and then choose, for each property, which method you'd like to use to verify it -- deductive proofs, model checking, static analysis, concolic tests.
What practical distinction are you drawing here? Surely with any approach you either have a fully sound proof of a given proposition, or you have a potentially unsound proposition that you've tested at whatever level you feel appropriate. Like, if I have a SortedList type that can produce an assertion that, given n <= m, l[n] <= l[m], either the constructors of SortedList bake that in as a deductive proof, or they unsoundly assert it and I apply some level of static analysis and/or testing to them - how's that any different from what I'd do using any other technique?
> 4. Because dependent types are so tied to the program, the program must be written with the specific properties you want to verify in mind. If, after writing the program, you want to prove other properties about it, you'll probably need to rewrite it.
I'm not entirely convinced that this is any harder than any other approach - you'd have to propagate the new properties you were interested in through the code, sure, which would likely involve changing the types that the relevant points in the program were annotated with. But isn't it much the same process with a detached proof of the program property?
Hercuros|6 years ago
One major benefit that proof assistants have over other formal methods is that they can be used to prove essentially arbitrary properties of programs, which is not true of any automated methods. Basically, if we as humans are able to convince ourselves that a program has a certain property, then we could also show this using a (dependently-typed) proof assistant.
(Yes, theoretically all proof systems have limitations due to Gödel’s incompleteness theorem, but this limitation applies just the same to ALL formal methods. Furthermore, you’re not that likely to run into it in practice unless you are doing metatheory, and even there many interesting statements CAN still be shown.)
Consider the formally verified C compiler CompCert, where the assembly output of the compiler has been proven to have the same behavior as the input source code. A proof like this simply cannot be done using automated methods currently, and requires human assistance. This kind of correctness proof is also highly non-compositional, since the correctness proof of a compiler does not mirror the structure of the compiler very closely. Hence this also invalidates your point about dependent types not being able to handle non-compositional properties very well. There are plenty of other examples, like the seL4 microkernel.
I also do not understand what bearing computational complexity results have on humans manually formalizing their informal intuitions about program correctness in a proof assistant. Humans do not work on arbitrary problems where they have no intuition at all about why a program is correct, hence referring to worst-case computational complexity results does not make much sense here. In fact, if you have no intuition about why a program works, then how did you manage to write it in the first place? You surely did not write random garbage in the hopes that you would get a working program.
You might say that there are programs you can check using a model checker, but which humans cannot reasonably keep in their heads or form an intuition about, and therefore these proofs cannot formalized in a proof assistant. But what you can do is implement a model checker in your proof assistant and then show that the model checker is correct. After you've done that, you can simply use the model checker to do your proofs for you. And of course it should be possible to formalize the model checker itself, since the people that wrote the model checker must have some intuition about why it works and produces the correct results. In this sense, proof assistants subsume all other formal methods, since they can be "scripted" to include them.
Furthermore, it is generally not the case that you have to rewrite your program in case you want to prove some more properties about it. You may be thinking of a programming style where the type of a program encodes all the properties you are interested in, but you can avoid this style where necessary, by separating your program and its correctness proof.