4 ms·

This is a very confusing thread for me. I think Idris -- while not exactly mainstream -- has shown that it's fine to treat type checking and types as a continu

This is a very confusing thread for me. I think Idris -- while not exactly mainstream -- has shown that it's fine to treat type checking and types as a continuum. There's nothing about dependent types that forces anybody to prove Goldbach's conjecture or anything of the sort. You, the programmer, get to choose just how rigorously you want your values to be specified, and if you really want you can ask for proof of the Riemann hypothesis, or you can ask for a... String. For me, that's the great thing about dependent types -- you, the programmer, get to choose how rigorous you want to be.

pron 7y ago
> has shown that it's fine to treat type checking and types as a continuum It has not shown that at all. That you can encode arbitrary propositions with dependent types has been known for many decades. That doing so is a feasible, affordable way to verify software correctness has yet to be shown by anyone, despite decades of attempts. > You, the programmer, get to choose just how rigorously you want your values to be specified But that's the problem. Specifying your software and verifying it are two different things. The last thing you want is to limit the rigor of your specification to the rigor of your verfication, especially if your verification is done with deductive proofs, as that's the most costly, least effective verification method. You want developers to choose the rigor of their specification and separately choose the rigor of verification. The main problem with dependent types is that they don't let you do that, and so force you to specify only stuff you can affordably prove, which is usually the simple stuff.
- agentultra 7y ago
  > It has not shown that at all. That you can encode arbitrary propositions with dependent types has been known for many decades. That doing so is a feasible, affordable way to verify software correctness has yet to be shown by anyone, despite decades of attempts. Well feasible is definitely a way I would characterize dependently typed deductive proofs. Compcert was a large achievement and produced a formally verified compiler back-end. Therefore it is definitely feasible to design software that is correct by construction using these methods. I think it's pretty reasonable to say that it's not yet affordable to verify all compiler back-ends this way. However I don't think the future where it is affordable is far off. Folks in the Lean community are making head way and learning from Compcert about how to model the semantics of C-like programs using new advances in type theory that will make it easier to verify such systems. Therefore I wouldn't discount Dependently Typed Haskell so completely. Verification methods work in a continuum and I use a few depending on the needs of the project. I often use TLA+ and sometimes I use Lean. One day I'd like to see synthesis get better for large-scale projects. That would be super cool.
  - pron 7y ago
    > Compcert was a large achievement and produced a formally verified compiler back-end. Therefore it is definitely feasible to design software that is correct by construction using these methods. CompCert is a very small program (1/5 of jQuery) and it's taken world-experts years of work. Its verification also wasn't really done using dependent types, but in Coq, a traditional proof assistant whose theory happens to be based on dependent types, but is much more similar in practice to, say, Isabelle/HOL than to Idris/dependent Haskell. > However I don't think the future where it is affordable is far off. Folks in the Lean community are making head way and learning from Compcert about how to model the semantics of C-like programs using new advances in type theory that will make it easier to verify such systems. It's been said to not be far off for 40 years now. Yet what can be verified with deductive proofs has remained, for decades, 2-3 order of magnitudes behind "ordinary" software, and the gap isn't closing. > Therefore I wouldn't discount Dependently Typed Haskell so completely. I'm not. I'm just saying that it's currently less promising than the main thrust of formal methods research (which focuses on automated methods much more than on deductive proofs) and that it is certainly nowhere near a point where it can be said to be "the future." I'm also pointing out that there are currently approaches that subsume dependent types -- have nearly all of their advantages and virtually none of their disadvantages (contract systems).

pron 7y ago

> has shown that it's fine to treat type checking and types as a continuum It has not shown that at all. That you can encode arbitrary propositions with dependent types has been known for many decades. That doing so is a feasible, affordable way to verify software correctness has yet to be shown by anyone, despite decades of attempts. > You, the programmer, get to choose just how rigorously you want your values to be specified But that's the problem. Specifying your software and verifying it are two different things. The last thing you want is to limit the rigor of your specification to the rigor of your verfication, especially if your verification is done with deductive proofs, as that's the most costly, least effective verification method. You want developers to choose the rigor of their specification and separately choose the rigor of verification. The main problem with dependent types is that they don't let you do that, and so force you to specify only stuff you can affordably prove, which is usually the simple stuff.

agentultra 7y ago
> It has not shown that at all. That you can encode arbitrary propositions with dependent types has been known for many decades. That doing so is a feasible, affordable way to verify software correctness has yet to be shown by anyone, despite decades of attempts. Well feasible is definitely a way I would characterize dependently typed deductive proofs. Compcert was a large achievement and produced a formally verified compiler back-end. Therefore it is definitely feasible to design software that is correct by construction using these methods. I think it's pretty reasonable to say that it's not yet affordable to verify all compiler back-ends this way. However I don't think the future where it is affordable is far off. Folks in the Lean community are making head way and learning from Compcert about how to model the semantics of C-like programs using new advances in type theory that will make it easier to verify such systems. Therefore I wouldn't discount Dependently Typed Haskell so completely. Verification methods work in a continuum and I use a few depending on the needs of the project. I often use TLA+ and sometimes I use Lean. One day I'd like to see synthesis get better for large-scale projects. That would be super cool.
- pron 7y ago
  > Compcert was a large achievement and produced a formally verified compiler back-end. Therefore it is definitely feasible to design software that is correct by construction using these methods. CompCert is a very small program (1/5 of jQuery) and it's taken world-experts years of work. Its verification also wasn't really done using dependent types, but in Coq, a traditional proof assistant whose theory happens to be based on dependent types, but is much more similar in practice to, say, Isabelle/HOL than to Idris/dependent Haskell. > However I don't think the future where it is affordable is far off. Folks in the Lean community are making head way and learning from Compcert about how to model the semantics of C-like programs using new advances in type theory that will make it easier to verify such systems. It's been said to not be far off for 40 years now. Yet what can be verified with deductive proofs has remained, for decades, 2-3 order of magnitudes behind "ordinary" software, and the gap isn't closing. > Therefore I wouldn't discount Dependently Typed Haskell so completely. I'm not. I'm just saying that it's currently less promising than the main thrust of formal methods research (which focuses on automated methods much more than on deductive proofs) and that it is certainly nowhere near a point where it can be said to be "the future." I'm also pointing out that there are currently approaches that subsume dependent types -- have nearly all of their advantages and virtually none of their disadvantages (contract systems).