5 ms·

You don't need type theory to verify program properties, people have been using first-order methods for decades to prove properties about programs. For example

by jroesch 10y ago

You don't need type theory to verify program properties, people have been using first-order methods for decades to prove properties about programs. For example there was a line of work in ACL2 that verified a microprocessor implementation, as well as plenty of modern work using tools like SMT to automatically prove program properties, see Dafny, F* for language based approaches. Though there is plenty of language agnostic approaches as well. My colleagues at UW have a paper in this year's OSDI verifying crash consistency for a realistic file system with no manual proof.

catnaroek 10y ago
Nice. SMT can be (and indeed has been) integrated into type-based approaches to program verification as well.
- jroesch 10y ago
  Yeah I think SMT is really the state-of-the-art right now in this area. Leo De Moura (one of the main authors of Z3) has been working on Lean for the past couple of years. There is a small group of us (5~) who have been working on a big release for the past couple of months. The goal is to bring the easy of use of SMT automation to type theory, so you can get both the ability to do induction and automation. Lean: http://leanprover.github.io/ http://leanprover.github.io/
  - catnaroek 10y ago
    I wish you guys good luck. Freedom from Coq-style proof scripts should be the goal.
igravious 10y ago
If (like me) you didn't know what the abbreviation SMT stands for -- I looked it up and it is Shiver Me Timbers http://encyclopedia.thefreedictionary.com/Shiver+Me+Timbers http://encyclopedia.thefreedictionary.com/Shiver+Me+Timbers Seems to be some kind of pirate speak. Only kidding! It stands for Satisfiability Modulo Theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories “In computer science and mathematical logic, the satisfiability modulo theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming.” I'm not sure I'm any the wiser after that … A notable building block appears to be SMT-LIB http://smtlib.cs.uiowa.edu/index.shtml http://smtlib.cs.uiowa.edu/index.shtml

by jroesch 10y ago

catnaroek 10y ago

Nice. SMT can be (and indeed has been) integrated into type-based approaches to program verification as well.

jroesch 10y ago
Yeah I think SMT is really the state-of-the-art right now in this area. Leo De Moura (one of the main authors of Z3) has been working on Lean for the past couple of years. There is a small group of us (5~) who have been working on a big release for the past couple of months. The goal is to bring the easy of use of SMT automation to type theory, so you can get both the ability to do induction and automation. Lean: http://leanprover.github.io/ http://leanprover.github.io/
- catnaroek 10y ago
  I wish you guys good luck. Freedom from Coq-style proof scripts should be the goal.

igravious 10y ago

If (like me) you didn't know what the abbreviation SMT stands for -- I looked it up and it is Shiver Me Timbers http://encyclopedia.thefreedictionary.com/Shiver+Me+Timbers http://encyclopedia.thefreedictionary.com/Shiver+Me+Timbers Seems to be some kind of pirate speak. Only kidding! It stands for Satisfiability Modulo Theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories “In computer science and mathematical logic, the satisfiability modulo theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming.” I'm not sure I'm any the wiser after that … A notable building block appears to be SMT-LIB http://smtlib.cs.uiowa.edu/index.shtml http://smtlib.cs.uiowa.edu/index.shtml