4 ms·

Write a program to prove another one. It's pretty cool in concept, but is it useful in practice?

by didibus 10y ago

xj9 10y ago
TDD, formal verification i'd say yes
- didibus 10y ago
  I know TDD has gotten out of fashion, where people seem to acknowledge today that the right balance of tests is better, more practical, then a test first and test everything approach. Formal verification hasn't really caught on yet. The extra effort needed to formally prove even a trivial program seems to be too high for the value it gives to most stakeholders. I'm really hopeful for simpler methods of formalized proofs, or even automated testing. I think today, the practical cost is maybe still too high for people to care.
  - jononor 10y ago
    Property-based testing can sometimes be a practical step inbetween unit-testing and formal proofs. Scala is where this is most common/well-supported, I think http://www.scalatest.org/user_guide/property_based_testing http://www.scalatest.org/user_guide/property_based_testing
  - User23 10y ago
    Formal verification will never catch on, because it's silly and prohibitively difficult for all but the simplest programs. On the other hand, formal construction is an idea whose time is long overdue. Rather than asking if program text T satisfies predicate P, instead start with P and then construct a T mechanically such that it must satisfy P. The latter is a much easier task than the former. Sort of like how it's easy to know N is the product of two large primes if you just multiplied two large primes together to get it.
    - undershirt 10y ago
      How would we specify P? I can't get away from the idea that specifying P is similar to constructing T.
      - User23 10y ago
        Dijkstra and Scholten's Predicate Calculus and Program Semantics is a good textbook on the subject. Dijkstra's a Discipline of Programming is much more informal, but I find it more readable and it has a number of good examples.
        undershirt 10y ago
        This is probably difficult to explain without proper context, but could I ask you for a summary? (Thanks for the book references.)
ufo 10y ago
This isn't necessarily about proving other programs. It is about showing that at a very fundamental level, formal logic (as studied by logicians) and typed programming languages (as studied by computer scientists) are actually the same thing, but written in different ways. The basic idea is that there every typed programming language is analogous to a mathematical logic system and that * programs are analogous to logic statements (theorem) * a program's source code is equivalent to a proof of the theorem. * type-checking a program is equivalent to checking if a proof is correct. * Executing a program is equivalent to simplifying a proof. If we restrict ourselves to the sort of type systems in mainstream languages the logic statements that the types can express are somewhat limited and not very interesting. The proofs as programs analogy really starts getting interesting when you have a very powerful type system... One place where you see these powerful type systems is in the proof assistants for people who want to formalize mathematics. It turns out that writing proofs on these proof assistants is surprisingly similar to programming in a typed functional language! It is kind of interesting because all that you care about is that the program you write (the proof) type checks (is valid), and you don't actually ever run it. Coming closer to the software development side of things, some of these proof assistants can be used to produce formally verified software. Basically, what they do is that instead of throwing away the programs (proofs) that you write, they compile them down to executable code. This is not something that is very applicable to the general software population though since formal verification is a niche thing. It also doesn't help that these tools are currently super clunky to use and have a steep learning curve involving lots of difficult math.
- didibus 10y ago
  Hum, admittedly, most of this is past my knowledge graph, since I know nothing of mathematical logic. Are you saying the practical relevancy here is actually to logicians? In that it means they can now more easily come up with proofs for their theorems by simply writing a program instead of whatever more complicated paper proof they used to have to come up with? And that for software, it's only helpful in special cases where you need to guarantee a small piece of logic is 100% correct?

Write a program to prove another one. It's pretty cool in concept, but is it useful in practice?

by didibus 10y ago

Write a program to prove another one. It's pretty cool in concept, but is it useful in practice?

xj9 10y ago

TDD, formal verification i'd say yes

didibus 10y ago
I know TDD has gotten out of fashion, where people seem to acknowledge today that the right balance of tests is better, more practical, then a test first and test everything approach. Formal verification hasn't really caught on yet. The extra effort needed to formally prove even a trivial program seems to be too high for the value it gives to most stakeholders. I'm really hopeful for simpler methods of formalized proofs, or even automated testing. I think today, the practical cost is maybe still too high for people to care.
- jononor 10y ago
  Property-based testing can sometimes be a practical step inbetween unit-testing and formal proofs. Scala is where this is most common/well-supported, I think http://www.scalatest.org/user_guide/property_based_testing http://www.scalatest.org/user_guide/property_based_testing
- User23 10y ago
  Formal verification will never catch on, because it's silly and prohibitively difficult for all but the simplest programs. On the other hand, formal construction is an idea whose time is long overdue. Rather than asking if program text T satisfies predicate P, instead start with P and then construct a T mechanically such that it must satisfy P. The latter is a much easier task than the former. Sort of like how it's easy to know N is the product of two large primes if you just multiplied two large primes together to get it.
  - undershirt 10y ago
    How would we specify P? I can't get away from the idea that specifying P is similar to constructing T.
    - User23 10y ago
      Dijkstra and Scholten's Predicate Calculus and Program Semantics is a good textbook on the subject. Dijkstra's a Discipline of Programming is much more informal, but I find it more readable and it has a number of good examples.
      - undershirt 10y ago
        This is probably difficult to explain without proper context, but could I ask you for a summary? (Thanks for the book references.)

ufo 10y ago

This isn't necessarily about proving other programs. It is about showing that at a very fundamental level, formal logic (as studied by logicians) and typed programming languages (as studied by computer scientists) are actually the same thing, but written in different ways. The basic idea is that there every typed programming language is analogous to a mathematical logic system and that * programs are analogous to logic statements (theorem) * a program's source code is equivalent to a proof of the theorem. * type-checking a program is equivalent to checking if a proof is correct. * Executing a program is equivalent to simplifying a proof. If we restrict ourselves to the sort of type systems in mainstream languages the logic statements that the types can express are somewhat limited and not very interesting. The proofs as programs analogy really starts getting interesting when you have a very powerful type system... One place where you see these powerful type systems is in the proof assistants for people who want to formalize mathematics. It turns out that writing proofs on these proof assistants is surprisingly similar to programming in a typed functional language! It is kind of interesting because all that you care about is that the program you write (the proof) type checks (is valid), and you don't actually ever run it. Coming closer to the software development side of things, some of these proof assistants can be used to produce formally verified software. Basically, what they do is that instead of throwing away the programs (proofs) that you write, they compile them down to executable code. This is not something that is very applicable to the general software population though since formal verification is a niche thing. It also doesn't help that these tools are currently super clunky to use and have a steep learning curve involving lots of difficult math.

didibus 10y ago
Hum, admittedly, most of this is past my knowledge graph, since I know nothing of mathematical logic. Are you saying the practical relevancy here is actually to logicians? In that it means they can now more easily come up with proofs for their theorems by simply writing a program instead of whatever more complicated paper proof they used to have to come up with? And that for software, it's only helpful in special cases where you need to guarantee a small piece of logic is 100% correct?