7 ms·

Isabelle is definitely type-based by any definition I could think of. Really it's more of a logic and TLA+ is model checker. If we want to do model checking the

by tel 11y ago

Isabelle is definitely type-based by any definition I could think of. Really it's more of a logic and TLA+ is model checker. If we want to do model checking then SMT solvers are in every half-sane dependency manager on the planet verifying build sets. I still stand by the idea that these tools should be more widely used. I also don't understand a position where they're in opposition to type theoretic approaches. Liquid Haskell extends Haskell types with an SMT silver and, frankly, most logics can import a proof with ease if you're willing to trust an external party.

pron 11y ago
> Isabelle is definitely type-based by any definition I could think of. It certainly has types, but I don't think it bases its proofs on type theory in the same way Coq/Agda do (but I really know nothing about it, so you may be absolutely right). > I still stand by the idea that these tools should be more widely used. I agree. But it's important to remember that correctness is often not boolean, and is often yet another requirement, which varies across domains and projects, and with it the effort to provide it. > I also don't understand a position where they're in opposition to type theoretic approaches. They're not. I simply stated that type-theoretic approaches (including Haskell) have so far gained little traction, that's all. If they one day become more popular -- I'm all for it. The problem is that proof assistants -- be they type-based or set based -- are rarely used, and the reason is that they are notoriously hard to use, and hardly ever justify the effort. That kind of effort for correctness is only justifiable in niche applications, so those tools will always be niche tools. There's just no-way, no-how you can realistically expect large swaths of the industry to adopt them (and I'm trying to be optimistically realistic rather than a wishful-thinker). Model checkers, OTOH, are qualitatively different, and are much closer to writing tests. If the industry could be trained to write automated tests (and that has contributed greatly to the rise in software quality we've seen since the nineties, when we had a "correctness crisis"), then it can be trained to write a formal spec (a "lightweight model" as Pamela Zave calls it, or an "exhaustively-testable pseudocode" as Leslie Lamport calls it) and run a model checker. It is both more applicable, much cheaper, and much more familiar than formal proofs, and so it has a real chance at adoption. Dropping costs of computation have made it far more practical, too, for ever larger models.
- catnaroek 11y ago
  Model checkers, OTOH, are limited in scope, and can only work with finite domains, and, furthermore, is usually restricted to first-order reasoning on them. As soon as you want to prove anything slightly more interesting (e.g., «this nontrivial program transformation preserves the meaning of programs», or «this implementation of serializable database transactions protects the data integrity invariants of any relational database schema»), you're completely out of luck.
  - pron 11y ago
    Oh, certainly! But I still see little chance of proof assistants being used in the industry for anything but the most exotic niches. They're just too hard and time-consuming to use. Academics might certainly use them to prove algorithms as they prove algorithms now (although, at present, I also don't see too much realistic chance of algorithms requiring proof-assistants for their proof being implemented in the industry; as it is, even informally-proven algorithms that are complex enough and hard-enough to implement are avoided, and very few niches can afford translation validation for their implementation[1]) But, "this implementation of serializable database transactions protects the data integrity invariants of any relational database schema" can very well be verified by model checker on a finite model for some schemas (there's little reason to believe that serializability would be affected too much by schema, other than by the graph of foreign keys), and that may be enough to gain the necessary amount of confidence in the algorithm. I can certainly see distributed-database designers using model checkers for that. [1]: http://www.cl.cam.ac.uk/~mom22/pldi13.pdf http://www.cl.cam.ac.uk/~mom22/pldi13.pdf
    - catnaroek 11y ago
      «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.
      - 11y ago

by tel 11y ago

pron 11y ago

> Isabelle is definitely type-based by any definition I could think of. It certainly has types, but I don't think it bases its proofs on type theory in the same way Coq/Agda do (but I really know nothing about it, so you may be absolutely right). > I still stand by the idea that these tools should be more widely used. I agree. But it's important to remember that correctness is often not boolean, and is often yet another requirement, which varies across domains and projects, and with it the effort to provide it. > I also don't understand a position where they're in opposition to type theoretic approaches. They're not. I simply stated that type-theoretic approaches (including Haskell) have so far gained little traction, that's all. If they one day become more popular -- I'm all for it. The problem is that proof assistants -- be they type-based or set based -- are rarely used, and the reason is that they are notoriously hard to use, and hardly ever justify the effort. That kind of effort for correctness is only justifiable in niche applications, so those tools will always be niche tools. There's just no-way, no-how you can realistically expect large swaths of the industry to adopt them (and I'm trying to be optimistically realistic rather than a wishful-thinker). Model checkers, OTOH, are qualitatively different, and are much closer to writing tests. If the industry could be trained to write automated tests (and that has contributed greatly to the rise in software quality we've seen since the nineties, when we had a "correctness crisis"), then it can be trained to write a formal spec (a "lightweight model" as Pamela Zave calls it, or an "exhaustively-testable pseudocode" as Leslie Lamport calls it) and run a model checker. It is both more applicable, much cheaper, and much more familiar than formal proofs, and so it has a real chance at adoption. Dropping costs of computation have made it far more practical, too, for ever larger models.

catnaroek 11y ago
Model checkers, OTOH, are limited in scope, and can only work with finite domains, and, furthermore, is usually restricted to first-order reasoning on them. As soon as you want to prove anything slightly more interesting (e.g., «this nontrivial program transformation preserves the meaning of programs», or «this implementation of serializable database transactions protects the data integrity invariants of any relational database schema»), you're completely out of luck.
- pron 11y ago
  Oh, certainly! But I still see little chance of proof assistants being used in the industry for anything but the most exotic niches. They're just too hard and time-consuming to use. Academics might certainly use them to prove algorithms as they prove algorithms now (although, at present, I also don't see too much realistic chance of algorithms requiring proof-assistants for their proof being implemented in the industry; as it is, even informally-proven algorithms that are complex enough and hard-enough to implement are avoided, and very few niches can afford translation validation for their implementation[1]) But, "this implementation of serializable database transactions protects the data integrity invariants of any relational database schema" can very well be verified by model checker on a finite model for some schemas (there's little reason to believe that serializability would be affected too much by schema, other than by the graph of foreign keys), and that may be enough to gain the necessary amount of confidence in the algorithm. I can certainly see distributed-database designers using model checkers for that. [1]: http://www.cl.cam.ac.uk/~mom22/pldi13.pdf http://www.cl.cam.ac.uk/~mom22/pldi13.pdf
  - catnaroek 11y ago
    «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.
    - 11y ago