4 ms·

Just thinking out loud: if a program can check the correctness of another program against a formal spec, can't it just write the checked program from the spec?

dougws 10y ago
You've just invented the field of program synthesis, which is a super active research area right now in programming languages! Here's the paper list from a class at UW focused on this area: http://courses.cs.washington.edu/courses/cse599a2/15wi/ http://courses.cs.washington.edu/courses/cse599a2/15wi/ . The Sumit Gulwani paper from the first week is a really good introduction to the field.
derkha 10y ago
Aside from program synthesis, there is the more restricted form of code extraction, which turns definitions inside a theorem prover into code in a more traditional, runnable language such as OCaml. But you'll still want to do one or more refinement steps inside the theorem prover where you turn your spec into more efficient definitions (or even definitions that are computable at all - how do you evaluate an unbounded universal quantifier?)
stale2002 10y ago
Well then the spec isn't just a spec. It is a programming language in and of itself. And how do you prove that THAT spec is correct? It is turtle specs all the way down.
- Crespyl 10y ago
  Sooner or later your spec language is just English and you have to get the lawyers involved. ;)
usgroup 10y ago
Have a look at Why3 for example or Coq. That's exactly what formal verification systems do: 1. Formally prove intention. 2. Generate code.
MrManatee 10y ago
As others have already replied, sometimes it can. But sometimes, and particularly if we care about efficiency, this is so difficult that we're not even close to being able to automate it. For example, here is my "formal definition" of a primality checker: IsPrime(Int n) = n > 1 and not(exists a, b in Int: a > 1 and b > 1 and a * b == n) It is not directly executable, because it uses the "exists" quantifier over all integers. A clever code extractor should be able to somehow convert this to a finite computation. But would it be able to come up with the polynomial-time AKS primality test? [1] I highly doubt it. Unless, of course, there is a special case for recognizing this particular definition. But I don't think that really counts, because I'm only using primality checking as an example. You can't have a special case for everything. [1] https://en.wikipedia.org/wiki/AKS_primality_test https://en.wikipedia.org/wiki/AKS_primality_test
- AstralStorm 10y ago
  Actually, Isabelle has methods that check isomorphism of proofs in a brute force way. It is pretty slow, so it is almost always better to just say what specific proof you want to use.

dougws 10y ago

You've just invented the field of program synthesis, which is a super active research area right now in programming languages! Here's the paper list from a class at UW focused on this area: http://courses.cs.washington.edu/courses/cse599a2/15wi/ http://courses.cs.washington.edu/courses/cse599a2/15wi/ . The Sumit Gulwani paper from the first week is a really good introduction to the field.

derkha 10y ago

Aside from program synthesis, there is the more restricted form of code extraction, which turns definitions inside a theorem prover into code in a more traditional, runnable language such as OCaml. But you'll still want to do one or more refinement steps inside the theorem prover where you turn your spec into more efficient definitions (or even definitions that are computable at all - how do you evaluate an unbounded universal quantifier?)

stale2002 10y ago

Well then the spec isn't just a spec. It is a programming language in and of itself. And how do you prove that THAT spec is correct? It is turtle specs all the way down.

Crespyl 10y ago
Sooner or later your spec language is just English and you have to get the lawyers involved. ;)

usgroup 10y ago

Have a look at Why3 for example or Coq. That's exactly what formal verification systems do: 1. Formally prove intention. 2. Generate code.

MrManatee 10y ago

As others have already replied, sometimes it can. But sometimes, and particularly if we care about efficiency, this is so difficult that we're not even close to being able to automate it. For example, here is my "formal definition" of a primality checker: IsPrime(Int n) = n > 1 and not(exists a, b in Int: a > 1 and b > 1 and a * b == n) It is not directly executable, because it uses the "exists" quantifier over all integers. A clever code extractor should be able to somehow convert this to a finite computation. But would it be able to come up with the polynomial-time AKS primality test? [1] I highly doubt it. Unless, of course, there is a special case for recognizing this particular definition. But I don't think that really counts, because I'm only using primality checking as an example. You can't have a special case for everything. [1] https://en.wikipedia.org/wiki/AKS_primality_test https://en.wikipedia.org/wiki/AKS_primality_test

AstralStorm 10y ago
Actually, Isabelle has methods that check isomorphism of proofs in a brute force way. It is pretty slow, so it is almost always better to just say what specific proof you want to use.