3 ms·

People are missing the point of your post, which is a bit of a shame. The point is that `foo p n` returns an integer when `n` is the sum of two positive intege

by tome 7y ago

People are missing the point of your post, which is a bit of a shame. The point is that `foo p n` returns an integer when `n` is the sum of two positive integers that both satisfy `p`. `bar n` holds when `n` is prime. Thus `foo bar` always returns an integer iff Goldbach's conjecture is true. You point is that no one knows how to prove Goldbach's conjecture therefore no formal methods can prove that `foo bar` never crashes. If the dependent typing proponents in this thread responded to your point rather than picking holes in your usage of the words "composition" and "terminate" then they might make some interesting counterpoints. For example, they might say 1. "We don't expect dependent types to be able to prove everything (of course), we only expect them to be approximately as good as any other proof method for almost any property of interest", or 2. "What do you mean "you can easily prove almost any property of interest about each of them in isolation"? Does "property of interest" have a specific definition? How about `bar (factorial (10101010))`? Is that `True`? Is it not a "property of interest"? Is it not "in isolation"? How about "there exists n such that `bar m == False` for all m > n"? How would you "easily" prove that? Personally I'm not a dependent typing proponent so 1 is just my wild speculation. I am interested in your response to 2 though.

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.

by tome 7y ago

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.