26 ms·

The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations -- both in theory and in p

by pron 7y ago

The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations -- both in theory and in practice -- that the author does not seem to be aware of. He also does not seem to be aware of all the other approaches for software verification and correctness (sound static analysis, model checking, concolic testing) that have so far shown greater promise, and formal methods research focuses on them rather than on dependent types (the approach that scales least and suffers from the most limitations); in fact, last I spoke with a dependent type researchers, he told me that now they're trying to weaken the soundness of their type systems (sort of gradual-dependent-types) to try and fight the problems types suffer from. I'm not saying dependent types don't have some uses, or that they won't change enough so they could play a central role in software correctness, but thinking that they're the future of software correctness (in their current form) shows a complete lack of familiarity with this field.

tav 7y ago
Could you elaborate on the "fundamental, serious limitations" by any chance?
- 9q9 7y ago
  1. No type inference (unlike ML-style types). 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 7y ago
    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.
    - 9q9 7y ago
      1. BIdirectional isn't magic. If I program MergeSort or Quicksort, and give it the signature forall T. Array[T] -> (T -> T -> Bool) -> Array[T] Bidirectional will not infer what's missing towards a full spec. 2. Yes, you can refine later, but if you want to refine later (and in practise you almost always have the full spec -- if it exists at all -- only at the end), then why pay the cost of dependent types from the start? Once you have the full spec, verify with Hoare logic. 3, 4: I'm not sufficiently familiar with Idris to comment. 5. Alternative approaches, in addition owhat "pron" mentioned includes program logic, e.g. TLA.
      - hope-striker 7y ago
        1. Yes, but the situation regarding type inference is only a bit worse than the situation in non-dependently-typed languages. Of course the compiler can't magically figure out what theorems you want to prove.
        9q9 7y ago
        This is my point. Adding dependent types comes with costs that you will always have to pay, even if you don't use the power of dependent types. If you verify with e.g. program logic in the few real-world cases where formal verification is financially viable, then you only pay the price when you do the verification.
- pron 7y ago
  Sure. 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 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.
ernst_klim 7y ago
> The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations It would be great if you've mentioned them and briefly described why are they limiting. > model checking Is extremely complex. Proving complex programs using constrain solving would be too expensive, if possible. I would argue that proving stuff manually using SMT for trivial cases, as F* does, would be much more productive than doing the whole proof using any sort of constrain solver (if this would ever work for a sufficiently big program). The main problem of a constrain solvers is that they don't scale well. When you proved lemmas for a small block of code, you simply reuse those for higher order proofs. Constraints are being accumulated (tho not linearly) when the program grow and so does its state.
- pron 7y ago
  > It would be great if you've mentioned them and briefly described why are they limiting. I've done so here: https://news.ycombinator.com/item?id=20714845 https://news.ycombinator.com/item?id=20714845 > Is extremely complex. Proving complex programs using constrain solving would be too expensive, if possible. The same is true for deductive proofs, of which dependent types are a particular instance, only the problem is far worse. It is true that there are cases where deductive proofs are more feasible than model checking, but the converse is true in a much wider portion of cases. That's why deductive proofs are rarely the first choice, and they're used selectively, usually only after other methods have failed. Overall, deductive proof, although it certainly has its place in certain circumstances, is the least scalable verification method we have. This means that it's the last method you want to use by default, let alone bake it into your type system. > Constraints are being accumulated (tho not linearly) when the program grow and so does its state. This is true regardless of the verification method used. See my blog post here: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity > When you proved lemmas for a small block of code, you simply reuse those for higher order proofs. No, you can't "simply" reuse results. Here's an example (given in the post in Java, my preferred language, but as this is a post about Haskell, let me show it in Haskell): foo :: (Integer -> Bool) -> Integer -> Integer foo p x | x <= 2 || odd x = 0 | otherwise = head [i | i <- [x, x-1 .. 1], (p i) && p (x - i)] bar :: Integer -> Bool bar x = null [1 | i <- [x-1, x-2 .. 2], s <- [x, x-i .. 0], s == 0] These two subroutines are very simple, clearly terminating, and you can easily prove almost any property of interest about each of them in isolation. But now I claim that their composition `foo bar` never crashes (on `head`); can you prove me right or wrong? Feel free to "simply" reuse any proof about any of them. The idea that properties compose and that you can cheaply reuse knowledge about components to prove stuff about their composition is just mathematically false. There are a couple of results I mention in my blog posts that show that. We know that if you have a composition of components X_1 ∘ ... ∘ X_n then the cost of verifying some property of their composition is not only not polynomial in n, it's not even exponential in n (it's not any computable function in n, I think). I.e. it is a mathematical result that you cannot, generally, hide the complexity of components to make verification of their compsition scale with their number.
Ericson2314 7y ago
Every such thread we have pron disliking type theory vemenently. It just makes me chuckle now.
- pron 7y ago
  Not only do I not dislike type theory vehemently, I really like some of its uses (like linear types; don't believe me? I praised them in a recent talk: https://youtu.be/r6P0_FDr53Q?t=553 https://youtu.be/r6P0_FDr53Q?t=553). I'm not too fond of deductive proofs as a software verification method because so far it manages to scale worse than other formal methods (that don't scale that well, either). What I strongly dislike is: 1. Fetishization of certain formalisms, particularly combined with a rather limited understanding of said formalisms or formal systems in general. 2. Appeals to "the power of math" (mathiness) when discussing the extremely complex disciplines of engineering, especially when combined with a very limited knowledge of math. 3. Claims of the sort, "I like A more than B, hence I conclude that A is the best thing in the world", especially when combined with little knowledge of C or D (or A and B, really). And I don't like cults. It just so happens that those qualities are common among those who claim to particularly like type theory or functional programming (or, at least, among those who publicly talk or write about them). I don't think it's accidental, either. I think that some luminaries in that field encourage that kind of cult-of-magical-mathiness behavior, so this sort of thinking has become a part of the ethos of that community.
  - Ericson2314 7y ago
    There is more cult than cult leader. The people who enjoy functional programming find it vastly enjoyable/better/whatever. I fully admit it's hard to convey this and hard to demonstrate this empirically because the cost and scale of an adequate experiment would be prohibitive. The biggest thing I don't like about the model checkers and other strategies is: 1. No separation of proof and proof search. Deductive proofs are a good lingua franca. I want to mix and match techniques to derive the proofs and have them work together. Many of the things you like have potential to be repurposed as such "tactics". 2. Composition of verified programs. Functional programers really value composition and the things you like tend to be used for "whole progra verification". At the very least, while one can verify individual parts, there is no mechanized way to combine those proofs. I also think the evidence already points away from your scale argument. To put it simply, right now Agda is good for toy stuff, things you like are good for medium stuff, but only Coq and Isabelle/HOL is used for the biggest projects like Cake ML and Comp Cert. Both of those are proof theoretic tools.
dominotw 7y ago
I wonder why clojure's spec idea isn't being discussed that much. Having wrestled with scala's type system for like a decade, it all seems so pointless and stupid when compared to spec. At the time I thought this scala type system stuff was so advanced and scientific. So embarrassing to ppl who push this stuff.
- Scarbutt 7y ago
  Because clojure's spec is nothing new? programmers in dynamic langs have being doing it for ever, spec just gives you a framework to save on boilerplate. Also, spec's runtime performance is atrocious.
  - dominotw 7y ago
    > spec just gives you a framework to save on boilerplate. > spec's runtime performance is atrocious. How is that though? If you are reading stuff off of database/api you still have to do the same datavalidation even in scala, for example. I might be misunderstanding what you are saying but what runtime data validation have specifically do with spec.
  - pron 7y ago
    > Because clojure's spec is nothing new? You're absolutely right, but dependent types are nothing new, either. They're just new to Haskell. So contract systems aren't new, but they're new to languages some people actually use (or rather, that a contract system is used by a non-vanishingly small set of programmers is new). > Also, spec's runtime performance is atrocious. Have you tried writing deductive proofs with dependent types? I think the point was about using spec for development, not for runtime validation.
  - fulafel 7y ago
    Can you give some concrete examples on older spec-like things in other languages? It's not really clear what aspects of spec you refer to with this. It's easy to miss the details that give it a quality of its own, like the composability, property based testing support, and preservation of extensibility in APIs if you just have a quick look at spec.
whateveracct 7y ago
I mean regardless..having dependent types in Haskell is going to come in handy in industry. It's obviously not the case that dependent types are strictly too costly to ever use.
LeanderK 7y ago
> The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations -- both in theory and in practice -- that the author does not seem to be aware of I don't want to argue with you on the theory side since I am not an expert, but I can assure you that Idris is a nice language to work with. I prefer haskell due not non-dependently typed stuff, but I think otherwise it clearly shows that a practical dependent programming language to do actual real-world work is possible and ergonomic. EDIT: I also don't think that verification is the main advantage of dependent types. Haskells type-system is already unsound (f:: a -> b, f=unsafeCoerce, the universal proving function). I like it because it makes it easy to express more complicated constraints in an ergonomic and approachable way and therefore make the compiler just accept less programs. I see it as minimizing the chance for stupid bugs and give the programmer more information about what's going on by providing richer types.
dwohnitmok 7y ago
Dependent Haskell is not sound (type in type, i.e. a type level version of Russell's Paradox, and lack of totality checking). Its primary purpose is not theorem proving per se, but rather unifying the explosion of GHC extensions that currently are weak approximations of a full dependently typed system. More than anything it is precisely an exercise in whether dependent types are useful even if you aren't getting 100% watertight assurances with them. Sure the article is a bit exuberant, but I think you're being a bit harsh here. Yes the field of formal verification, from my amateur practitioner's point of view, is a mishmash of techniques right now, with no single technique that has quite the right ergonomic vs power ratio that dominates over all others. But as far as I can tell there is in fact a significant amount research being done in dependent types. Many programming languages now have very limited dependent types. GADTs are one form that shows up in e.g. OCaml, Haskell, and Scala. Indeed Jane Street had a blog post about how GADTs were surprisingly useful for them (https://blog.janestreet.com/why-gadts-matter-for-performance/ https://blog.janestreet.com/why-gadts-matter-for-performance...). Ongoing research projects occur for languages such as Agda and Coq. Just like with formal specification systems like TLA+ and Alloy where you don't need to specify in exhaustive detail what you're after to see significant value, you don't have to prove comprehensive theorems to derive significant value from dependent types. An easy, lightweight win is to leave behind value specific tokens when performing some sort of runtime check rather than trying to prove the runtime check (e.g. keeping track that yes I ran the isPrime function on this number, rather than proving that a number is actually prime), which you can then use to subsume pre/postcondition contract systems, since you can attach markers of arbitrary checks being made that don't necessarily affect the value (e.g. keep track that I did check this user ID against a blacklist before trying to use it elsewhere). The main problem with dependent types as far as I can tell is that only very recently have we had languages that try to write actual programs with full-spectrum dependent types appear. Idris is really the only example I can think of. Languages like Agda are first and foremost provers. I suspect the vast majority of Agda programs are never run after they've typechecked. As a result we have little idea of what good practices with full-spectrum dependent types looks like. I have suspicions it looks fairly different from the hacks that current statically typed languages try to use to approximate it. For example I suspect some correct by construction approaches to ordinary statically typed FP languages quickly spiral into monstrosities with full-spectrum dependent types that can be nicely sidestepped again with evidence of runtime checks instead of full proofs. Even with Idris, we don't have people using these systems in anger. We don't know how much to expose of function implementations, how much a totality checker matters, how best to avoid proof infection (where because a low-level component demands a proper proof and that proof is used at runtime, you must deliver a valid proof and can't use some sort of TrustMe escape hatch of a null value that has any type). There are ideas. Idris 2 introduces a type system that distinguishes between proofs that are never used at runtime and runtime values, allowing users to safely use the TrustMe escape hatch if necessary. But there isn't a large community working with them while trying to ship business products. That for me is the greatest promise of dependent types in Haskell. Getting more real world experience of programmers using dependent types to uncover ergonomic holes. The Haskell community in the grand scheme of languages is small. It is nonetheless orders of magnitude larger than the full-spectrum dependently typed community and, if Dependent Haskell lands, represents perhaps the first time that a dependently typed language is used to directly write, rather than verify, production systems.
willtim 7y ago
I think the title is tongue-in-cheek. Clearly the future is Python and JavaScript.

by pron 7y ago

tav 7y ago

Could you elaborate on the "fundamental, serious limitations" by any chance?

9q9 7y ago
1. No type inference (unlike ML-style types). 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 7y ago
  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.
  - 9q9 7y ago
    1. BIdirectional isn't magic. If I program MergeSort or Quicksort, and give it the signature forall T. Array[T] -> (T -> T -> Bool) -> Array[T] Bidirectional will not infer what's missing towards a full spec. 2. Yes, you can refine later, but if you want to refine later (and in practise you almost always have the full spec -- if it exists at all -- only at the end), then why pay the cost of dependent types from the start? Once you have the full spec, verify with Hoare logic. 3, 4: I'm not sufficiently familiar with Idris to comment. 5. Alternative approaches, in addition owhat "pron" mentioned includes program logic, e.g. TLA.
    - hope-striker 7y ago
      1. Yes, but the situation regarding type inference is only a bit worse than the situation in non-dependently-typed languages. Of course the compiler can't magically figure out what theorems you want to prove.
      - 9q9 7y ago
        This is my point. Adding dependent types comes with costs that you will always have to pay, even if you don't use the power of dependent types. If you verify with e.g. program logic in the few real-world cases where formal verification is financially viable, then you only pay the price when you do the verification.
pron 7y ago
Sure. 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 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.

ernst_klim 7y ago

> The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations It would be great if you've mentioned them and briefly described why are they limiting. > model checking Is extremely complex. Proving complex programs using constrain solving would be too expensive, if possible. I would argue that proving stuff manually using SMT for trivial cases, as F* does, would be much more productive than doing the whole proof using any sort of constrain solver (if this would ever work for a sufficiently big program). The main problem of a constrain solvers is that they don't scale well. When you proved lemmas for a small block of code, you simply reuse those for higher order proofs. Constraints are being accumulated (tho not linearly) when the program grow and so does its state.

pron 7y ago
> It would be great if you've mentioned them and briefly described why are they limiting. I've done so here: https://news.ycombinator.com/item?id=20714845 https://news.ycombinator.com/item?id=20714845 > Is extremely complex. Proving complex programs using constrain solving would be too expensive, if possible. The same is true for deductive proofs, of which dependent types are a particular instance, only the problem is far worse. It is true that there are cases where deductive proofs are more feasible than model checking, but the converse is true in a much wider portion of cases. That's why deductive proofs are rarely the first choice, and they're used selectively, usually only after other methods have failed. Overall, deductive proof, although it certainly has its place in certain circumstances, is the least scalable verification method we have. This means that it's the last method you want to use by default, let alone bake it into your type system. > Constraints are being accumulated (tho not linearly) when the program grow and so does its state. This is true regardless of the verification method used. See my blog post here: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity > When you proved lemmas for a small block of code, you simply reuse those for higher order proofs. No, you can't "simply" reuse results. Here's an example (given in the post in Java, my preferred language, but as this is a post about Haskell, let me show it in Haskell): foo :: (Integer -> Bool) -> Integer -> Integer foo p x | x <= 2 || odd x = 0 | otherwise = head [i | i <- [x, x-1 .. 1], (p i) && p (x - i)] bar :: Integer -> Bool bar x = null [1 | i <- [x-1, x-2 .. 2], s <- [x, x-i .. 0], s == 0] These two subroutines are very simple, clearly terminating, and you can easily prove almost any property of interest about each of them in isolation. But now I claim that their composition `foo bar` never crashes (on `head`); can you prove me right or wrong? Feel free to "simply" reuse any proof about any of them. The idea that properties compose and that you can cheaply reuse knowledge about components to prove stuff about their composition is just mathematically false. There are a couple of results I mention in my blog posts that show that. We know that if you have a composition of components X_1 ∘ ... ∘ X_n then the cost of verifying some property of their composition is not only not polynomial in n, it's not even exponential in n (it's not any computable function in n, I think). I.e. it is a mathematical result that you cannot, generally, hide the complexity of components to make verification of their compsition scale with their number.

Ericson2314 7y ago

Every such thread we have pron disliking type theory vemenently. It just makes me chuckle now.

pron 7y ago
Not only do I not dislike type theory vehemently, I really like some of its uses (like linear types; don't believe me? I praised them in a recent talk: https://youtu.be/r6P0_FDr53Q?t=553 https://youtu.be/r6P0_FDr53Q?t=553). I'm not too fond of deductive proofs as a software verification method because so far it manages to scale worse than other formal methods (that don't scale that well, either). What I strongly dislike is: 1. Fetishization of certain formalisms, particularly combined with a rather limited understanding of said formalisms or formal systems in general. 2. Appeals to "the power of math" (mathiness) when discussing the extremely complex disciplines of engineering, especially when combined with a very limited knowledge of math. 3. Claims of the sort, "I like A more than B, hence I conclude that A is the best thing in the world", especially when combined with little knowledge of C or D (or A and B, really). And I don't like cults. It just so happens that those qualities are common among those who claim to particularly like type theory or functional programming (or, at least, among those who publicly talk or write about them). I don't think it's accidental, either. I think that some luminaries in that field encourage that kind of cult-of-magical-mathiness behavior, so this sort of thinking has become a part of the ethos of that community.
- Ericson2314 7y ago
  There is more cult than cult leader. The people who enjoy functional programming find it vastly enjoyable/better/whatever. I fully admit it's hard to convey this and hard to demonstrate this empirically because the cost and scale of an adequate experiment would be prohibitive. The biggest thing I don't like about the model checkers and other strategies is: 1. No separation of proof and proof search. Deductive proofs are a good lingua franca. I want to mix and match techniques to derive the proofs and have them work together. Many of the things you like have potential to be repurposed as such "tactics". 2. Composition of verified programs. Functional programers really value composition and the things you like tend to be used for "whole progra verification". At the very least, while one can verify individual parts, there is no mechanized way to combine those proofs. I also think the evidence already points away from your scale argument. To put it simply, right now Agda is good for toy stuff, things you like are good for medium stuff, but only Coq and Isabelle/HOL is used for the biggest projects like Cake ML and Comp Cert. Both of those are proof theoretic tools.

dominotw 7y ago

I wonder why clojure's spec idea isn't being discussed that much. Having wrestled with scala's type system for like a decade, it all seems so pointless and stupid when compared to spec. At the time I thought this scala type system stuff was so advanced and scientific. So embarrassing to ppl who push this stuff.

Scarbutt 7y ago
Because clojure's spec is nothing new? programmers in dynamic langs have being doing it for ever, spec just gives you a framework to save on boilerplate. Also, spec's runtime performance is atrocious.
- dominotw 7y ago
  > spec just gives you a framework to save on boilerplate. > spec's runtime performance is atrocious. How is that though? If you are reading stuff off of database/api you still have to do the same datavalidation even in scala, for example. I might be misunderstanding what you are saying but what runtime data validation have specifically do with spec.
- pron 7y ago
  > Because clojure's spec is nothing new? You're absolutely right, but dependent types are nothing new, either. They're just new to Haskell. So contract systems aren't new, but they're new to languages some people actually use (or rather, that a contract system is used by a non-vanishingly small set of programmers is new). > Also, spec's runtime performance is atrocious. Have you tried writing deductive proofs with dependent types? I think the point was about using spec for development, not for runtime validation.
- fulafel 7y ago
  Can you give some concrete examples on older spec-like things in other languages? It's not really clear what aspects of spec you refer to with this. It's easy to miss the details that give it a quality of its own, like the composability, property based testing support, and preservation of extensibility in APIs if you just have a quick look at spec.

whateveracct 7y ago

I mean regardless..having dependent types in Haskell is going to come in handy in industry. It's obviously not the case that dependent types are strictly too costly to ever use.

LeanderK 7y ago

> The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations -- both in theory and in practice -- that the author does not seem to be aware of I don't want to argue with you on the theory side since I am not an expert, but I can assure you that Idris is a nice language to work with. I prefer haskell due not non-dependently typed stuff, but I think otherwise it clearly shows that a practical dependent programming language to do actual real-world work is possible and ergonomic. EDIT: I also don't think that verification is the main advantage of dependent types. Haskells type-system is already unsound (f:: a -> b, f=unsafeCoerce, the universal proving function). I like it because it makes it easy to express more complicated constraints in an ergonomic and approachable way and therefore make the compiler just accept less programs. I see it as minimizing the chance for stupid bugs and give the programmer more information about what's going on by providing richer types.

dwohnitmok 7y ago

Dependent Haskell is not sound (type in type, i.e. a type level version of Russell's Paradox, and lack of totality checking). Its primary purpose is not theorem proving per se, but rather unifying the explosion of GHC extensions that currently are weak approximations of a full dependently typed system. More than anything it is precisely an exercise in whether dependent types are useful even if you aren't getting 100% watertight assurances with them. Sure the article is a bit exuberant, but I think you're being a bit harsh here. Yes the field of formal verification, from my amateur practitioner's point of view, is a mishmash of techniques right now, with no single technique that has quite the right ergonomic vs power ratio that dominates over all others. But as far as I can tell there is in fact a significant amount research being done in dependent types. Many programming languages now have very limited dependent types. GADTs are one form that shows up in e.g. OCaml, Haskell, and Scala. Indeed Jane Street had a blog post about how GADTs were surprisingly useful for them (https://blog.janestreet.com/why-gadts-matter-for-performance/ https://blog.janestreet.com/why-gadts-matter-for-performance...). Ongoing research projects occur for languages such as Agda and Coq. Just like with formal specification systems like TLA+ and Alloy where you don't need to specify in exhaustive detail what you're after to see significant value, you don't have to prove comprehensive theorems to derive significant value from dependent types. An easy, lightweight win is to leave behind value specific tokens when performing some sort of runtime check rather than trying to prove the runtime check (e.g. keeping track that yes I ran the isPrime function on this number, rather than proving that a number is actually prime), which you can then use to subsume pre/postcondition contract systems, since you can attach markers of arbitrary checks being made that don't necessarily affect the value (e.g. keep track that I did check this user ID against a blacklist before trying to use it elsewhere). The main problem with dependent types as far as I can tell is that only very recently have we had languages that try to write actual programs with full-spectrum dependent types appear. Idris is really the only example I can think of. Languages like Agda are first and foremost provers. I suspect the vast majority of Agda programs are never run after they've typechecked. As a result we have little idea of what good practices with full-spectrum dependent types looks like. I have suspicions it looks fairly different from the hacks that current statically typed languages try to use to approximate it. For example I suspect some correct by construction approaches to ordinary statically typed FP languages quickly spiral into monstrosities with full-spectrum dependent types that can be nicely sidestepped again with evidence of runtime checks instead of full proofs. Even with Idris, we don't have people using these systems in anger. We don't know how much to expose of function implementations, how much a totality checker matters, how best to avoid proof infection (where because a low-level component demands a proper proof and that proof is used at runtime, you must deliver a valid proof and can't use some sort of TrustMe escape hatch of a null value that has any type). There are ideas. Idris 2 introduces a type system that distinguishes between proofs that are never used at runtime and runtime values, allowing users to safely use the TrustMe escape hatch if necessary. But there isn't a large community working with them while trying to ship business products. That for me is the greatest promise of dependent types in Haskell. Getting more real world experience of programmers using dependent types to uncover ergonomic holes. The Haskell community in the grand scheme of languages is small. It is nonetheless orders of magnitude larger than the full-spectrum dependently typed community and, if Dependent Haskell lands, represents perhaps the first time that a dependently typed language is used to directly write, rather than verify, production systems.

willtim 7y ago

I think the title is tongue-in-cheek. Clearly the future is Python and JavaScript.