5 ms·

«few niches can afford translation validation»: So, as long as you can avoid it, don't translate. Perform your proofs in the same term language in which your pr

«few niches can afford translation validation»: So, as long as you can avoid it, don't translate. Perform your proofs in the same term language in which your program is written. «other than by the graph of foreign keys»: That's, like, the whole point to using relational databases.

pron 11y ago
> Perform your proofs in the same term language in which your program is written. We don't have such (real) languages yet[1]. Idris is far from being production ready and or demonstrating it can be effectively used for real-workd programs. Even then, it still remains to be shown that such languages will be cheaper to use than validating the translation and still be performant enough for the purpose they're used for (and, BTW, systems that require this level of correctness usually require proofs of timing and memory use -- including stack use). [1] There is actually one such language -- Esterel. It (and its descendants) have been used to write safety-critical software successfully. It's an incredible language, but it doesn't translate well to other domains as it's not Turing complete.
catnaroek 11y ago
> We don't have such (real) languages yet We do. Because Haskell and ML are ultimately just fancy term rewriting systems, you can do equational reasoning on their terms by hand just fine. It's even easy enough for non-[computer scientists/mathematicians] (such as yours truly) to do it casually!
- pron 11y ago
  Like I said above, Haskell/ML's type systems don't even come close to verifying most interesting program properties. They can't even verify a monad, let alone the simplest sorting (or selection) algorithm. All those software verification tools most certainly can, and even much more interesting properties/algorithms than that. Esterel can't verify a sorting algorithm (as it can't even express it), but it can verify most properties that interest developers of safety-critical control systems, including timing and memory use.
  - catnaroek 11y ago
    «can't verify a monad» (probably you meant «that the monad laws hold») More often than not, either the monad laws are easy to verify by hand (exceptions, state, nondeterminism, etc.) or the verification can be borrowed from nLab. It's a nonproblem. As I said in another comment, there's no general technique or tool for proving arbitrary theorems, and we have to live with that. Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy.
    - pron 11y ago
      > It's a nonproblem. And that's exactly what can be said about the difference between Haskell's and Java's type systems. It hasn't been shown that the additional provable properties -- that are not too powerful -- do in fact result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem. That requires empirical evidence. > Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy. But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
      - tome 11y ago
        > result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem I think there's too little agreement in this thread about what "cheaper" and "real problem" mean. I certainly find that Haskell "more cheaply" (i.e. with less mental burden) allows me, as an individual, to write programs more easily. Whether that observation scales to everyone is a very hard question to answer. > But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)? On the face of it, proving by manipulating Haskell expressions certainly compares favourably to proving with TLA+ and then translating into Haskell (or other language). There may, on the other hand, be additional tooling advantages around TLA+.

pron 11y ago

> Perform your proofs in the same term language in which your program is written. We don't have such (real) languages yet[1]. Idris is far from being production ready and or demonstrating it can be effectively used for real-workd programs. Even then, it still remains to be shown that such languages will be cheaper to use than validating the translation and still be performant enough for the purpose they're used for (and, BTW, systems that require this level of correctness usually require proofs of timing and memory use -- including stack use). [1] There is actually one such language -- Esterel. It (and its descendants) have been used to write safety-critical software successfully. It's an incredible language, but it doesn't translate well to other domains as it's not Turing complete.

catnaroek 11y ago

> We don't have such (real) languages yet We do. Because Haskell and ML are ultimately just fancy term rewriting systems, you can do equational reasoning on their terms by hand just fine. It's even easy enough for non-[computer scientists/mathematicians] (such as yours truly) to do it casually!

pron 11y ago
Like I said above, Haskell/ML's type systems don't even come close to verifying most interesting program properties. They can't even verify a monad, let alone the simplest sorting (or selection) algorithm. All those software verification tools most certainly can, and even much more interesting properties/algorithms than that. Esterel can't verify a sorting algorithm (as it can't even express it), but it can verify most properties that interest developers of safety-critical control systems, including timing and memory use.
- catnaroek 11y ago
  «can't verify a monad» (probably you meant «that the monad laws hold») More often than not, either the monad laws are easy to verify by hand (exceptions, state, nondeterminism, etc.) or the verification can be borrowed from nLab. It's a nonproblem. As I said in another comment, there's no general technique or tool for proving arbitrary theorems, and we have to live with that. Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy.
  - pron 11y ago
    > It's a nonproblem. And that's exactly what can be said about the difference between Haskell's and Java's type systems. It hasn't been shown that the additional provable properties -- that are not too powerful -- do in fact result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem. That requires empirical evidence. > Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy. But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
    - tome 11y ago
      > result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem I think there's too little agreement in this thread about what "cheaper" and "real problem" mean. I certainly find that Haskell "more cheaply" (i.e. with less mental burden) allows me, as an individual, to write programs more easily. Whether that observation scales to everyone is a very hard question to answer. > But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)? On the face of it, proving by manipulating Haskell expressions certainly compares favourably to proving with TLA+ and then translating into Haskell (or other language). There may, on the other hand, be additional tooling advantages around TLA+.