3 ms·

1. I mentioned why dependent types are not as good, in my opinion, as other verification methods. They are not flexible in the choice of verification method, an

by pron 7y ago

1. I mentioned why dependent types are not as good, in my opinion, as other verification methods. They are not flexible in the choice of verification method, and the method they're tied to is the worst default a programmer could want. 2. It's not a very precise statement, I mean that you can fully describe and understand what it is they do. After all, when you verify a program, you want to check certain properties that are of interest to you (because they're requirements). So you can ask and answer questions like what it is that they do, are there values of p for which foo always returns false? Values for which it always returns true? Values for which it sometimes returns true and sometimes false? And yes, your question, too, "there exists n such that `bar m == False` for all m > n?" The answer is no, and it was proven by Euclid: https://en.wikipedia.org/wiki/Euclid%27s_theorem https://en.wikipedia.org/wiki/Euclid%27s_theorem In other words, if two different programmers were writing foo and bar (as is often the case in software), each would have thought -- without knowing of the other component -- that pretty much any property they want to state about their component could be rather easily proven.

tome 7y ago
Regarding 2 I think you're missing my point. Firstly, the first "property of interest" was rendered incorrectly (and also stated incorrectly). It was supposed to be > How about `bar (factorial (10^10^10^10 + 1))`? Is that `True`? Can we easily prove or disprove that property of interest? Secondly, I know the second result is true. I'm asking how you would easily prove it. How do you easily show that "forall m. bar m == True" is equivalent to Euclid's theorem?
- pron 7y ago
  > Can we easily prove or disprove that property of interest? Maybe we could answer that affordably, albeit with some probability, using fast probabilistic primality tests (I don't know how high they can practically go). But can we easily prove what the result of sorting a particular list with a 10^10^10 elements is? Maybe not, but I don't think it's as much a property of interest as "does this program ever crash." In other words, for every algorithm with some non-trivial complexity, the question of what the result would be for some very large input is hard to answer, but I don't think that is a common property of interest. But if I get your meaning, you are correct that sometimes, if our focus is on an algorithm rather than on a working system, we forget that all systems can, at best, be shown correct only with some probability (because the hardware only does what it's told with probability), and at some point, there are algorithmic bugs that can occur in practice with a probability that's lower than that of a hardware glitch. > How do you easily show that "forall m. bar m == True" is equivalent to Euclid's theorem? By proving that bar is, indeed, a primality test, which is not hard. I.e. you prove that bar n = TRUE iff ∀ m ∈ ℕ . 1 < m < n ⇒ n % m ≠ 0. This is usually proven by induction.
Quekid5 7y ago
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.

by pron 7y ago

tome 7y ago

Regarding 2 I think you're missing my point. Firstly, the first "property of interest" was rendered incorrectly (and also stated incorrectly). It was supposed to be > How about `bar (factorial (10^10^10^10 + 1))`? Is that `True`? Can we easily prove or disprove that property of interest? Secondly, I know the second result is true. I'm asking how you would easily prove it. How do you easily show that "forall m. bar m == True" is equivalent to Euclid's theorem?

pron 7y ago
> Can we easily prove or disprove that property of interest? Maybe we could answer that affordably, albeit with some probability, using fast probabilistic primality tests (I don't know how high they can practically go). But can we easily prove what the result of sorting a particular list with a 10^10^10 elements is? Maybe not, but I don't think it's as much a property of interest as "does this program ever crash." In other words, for every algorithm with some non-trivial complexity, the question of what the result would be for some very large input is hard to answer, but I don't think that is a common property of interest. But if I get your meaning, you are correct that sometimes, if our focus is on an algorithm rather than on a working system, we forget that all systems can, at best, be shown correct only with some probability (because the hardware only does what it's told with probability), and at some point, there are algorithmic bugs that can occur in practice with a probability that's lower than that of a hardware glitch. > How do you easily show that "forall m. bar m == True" is equivalent to Euclid's theorem? By proving that bar is, indeed, a primality test, which is not hard. I.e. you prove that bar n = TRUE iff ∀ m ∈ ℕ . 1 < m < n ⇒ n % m ≠ 0. This is usually proven by induction.

Quekid5 7y ago

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.