3 ms·

> Before you can even consider verifying something, you have to be able to talk about it in some formal language. Sure, but it doesn't have to be a programming

> Before you can even consider verifying something, you have to be able to talk about it in some formal language. Sure, but it doesn't have to be a programming language. > Preferably the one you're programming in. Who says so? Programming languages (justifiedly) optimize for the ability to express computation, not the ability to express proof. In spite of Curry-Howard, there exist important differences between proofs and programs: (0) Proofs are primarily for humans to understand. Programs are primarily for computers to execute. (1) Proofs are sometimes allowed to be non-constructive. Even when they aren't, an easily understandable proof beats one that corresponds to an efficient program. (2) Allowing non-terminating programs is actually a good thing: it allows for proofs of correctness that use techniques not anticipated by the language designer. OTOH, if your logic lets you prove a contradiction, it's the end of the world (for your logic).

Animats 9y ago
Proofs and specifications are different things. Users need to be able to read specifications. For example, if you want to talk about definedness for arrays, a predicate defined(arrayname, lowbound, highbound) is helpful. That goes in assert statements. It's run-time checkable, if you have some extra state in the form of "is defined" flags. But you'd rather prove it once so the run-time checks are unnecessary. With a few simple theorems, such as defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) and a simple automated prover, you can deal with most of the issues around partially defined arrays. Think of proof support as being an extension to optimization of assertions. Most assertions in programs can be proven easily with an automated prover. Users need never see those proofs. Some will be hard and require more proof support.
- catnaroek 9y ago
  > That goes in assert statements. It's run-time checkable And runtime checks help because...? > But you'd rather prove it once so the run-time checks are unnecessary. No. I'd rather prove it to rule out the program being wrong. The runtime check is totally besides the point. > With a few simple theorems, such as (...) I think you mean “proposition”. It's not a theorem until it has been proven. > Think of proof support as being an extension to optimization of assertions. I never use runtime-checked assertions, so I never need to optimize them away. > Users need never see those proofs. But, you see, I want to see the proofs. How am I supposed to maintain a program I don't understand?
  - Animats 9y ago
    defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) is a theorem. It looks like this in Boyer-Moore theory: (PROVE-LEMMA arraytrue-extend-upward-rule (REWRITE) (IMPLIES (AND (EQUAL (arraytrue A I J) T) (EQUAL (alltrue (selecta A (ADD1 J))) T)) (EQUAL (arraytrue A I (ADD1 J)) T))) Name the conjecture *1. We will try to prove it by induction. There are three plausible inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (LESSP J I) (p A I J)) (IMPLIES (AND (NOT (LESSP J I)) (p A (ADD1 I) J)) (p A I J))). Linear arithmetic informs us that the measure (DIFFERENCE (ADD1 J) I) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to three new formulas: Case 3. (IMPLIES (AND (LESSP J I) (ARRAYTRUE A I J) (EQUAL (ALLTRUE (SELECTA A (ADD1 J))) T)) (ARRAYTRUE A I (ADD1 J))), which simplifies, rewriting with ARRAYTRUE-VOID-RULE and SUB1-ADD1, and opening up ARRAYTRUE and LESSP, to the following eight new conjectures: ... That finishes the proof of *1. Q.E.D. "arraytrue" is defined recursively: (DEFN arraytrue (A I J) (IF (LESSP J I) T -- the null case is true (AND (EQUAL (alltrue (selecta A I)) T) -- next element is true (arraytrue A (ADD1 I) J))) -- and rest of array is alltrue And yes, there's a machine proof that this terminates.
    - catnaroek 9y ago
      > defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) is a theorem. (proof) Sure. My point is just that a theorem is a proposition equipped with a proof. If the user just enters a proposition into the system, then they aren't entering a theorem. They're entering a proposition that the system can turn into a theorem.
  - kbenson 9y ago
    > > But you'd rather prove it once so the run-time checks are unnecessary. > No. I'd rather prove it to rule out the program being wrong. The runtime check is totally besides the point. That's the same thing. It's just a matter of it being automated. > > Think of proof support as being an extension to optimization of assertions. > I never use runtime-checked assertions, so I never need to optimize them away. If you've ever used a language that uses bounds checked array access, you have. IIRC, you've used Rust some, so you've used bounds checked array access, except where Rust was able to prove that out of bounds access was impossible and elide the code that checks. > > Users need never see those proofs. > But, you see, I want to see the proofs. How am I supposed to maintain a program I don't understand? There's a difference between need and ability. Just because it's stated you don't need to see something doesn't mean you can't. If you want to see a proof, you dig in and find it, or find where it's accepted canon that we don't need to reproduce (do we need proofs for integer addition? That seems of limited use to me, but maybe a formally proved as much as possible all the way to that level language has some interesting benefits).

Animats 9y ago

Proofs and specifications are different things. Users need to be able to read specifications. For example, if you want to talk about definedness for arrays, a predicate defined(arrayname, lowbound, highbound) is helpful. That goes in assert statements. It's run-time checkable, if you have some extra state in the form of "is defined" flags. But you'd rather prove it once so the run-time checks are unnecessary. With a few simple theorems, such as defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) and a simple automated prover, you can deal with most of the issues around partially defined arrays. Think of proof support as being an extension to optimization of assertions. Most assertions in programs can be proven easily with an automated prover. Users need never see those proofs. Some will be hard and require more proof support.

catnaroek 9y ago
> That goes in assert statements. It's run-time checkable And runtime checks help because...? > But you'd rather prove it once so the run-time checks are unnecessary. No. I'd rather prove it to rule out the program being wrong. The runtime check is totally besides the point. > With a few simple theorems, such as (...) I think you mean “proposition”. It's not a theorem until it has been proven. > Think of proof support as being an extension to optimization of assertions. I never use runtime-checked assertions, so I never need to optimize them away. > Users need never see those proofs. But, you see, I want to see the proofs. How am I supposed to maintain a program I don't understand?
- Animats 9y ago
  defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) is a theorem. It looks like this in Boyer-Moore theory: (PROVE-LEMMA arraytrue-extend-upward-rule (REWRITE) (IMPLIES (AND (EQUAL (arraytrue A I J) T) (EQUAL (alltrue (selecta A (ADD1 J))) T)) (EQUAL (arraytrue A I (ADD1 J)) T))) Name the conjecture *1. We will try to prove it by induction. There are three plausible inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (LESSP J I) (p A I J)) (IMPLIES (AND (NOT (LESSP J I)) (p A (ADD1 I) J)) (p A I J))). Linear arithmetic informs us that the measure (DIFFERENCE (ADD1 J) I) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to three new formulas: Case 3. (IMPLIES (AND (LESSP J I) (ARRAYTRUE A I J) (EQUAL (ALLTRUE (SELECTA A (ADD1 J))) T)) (ARRAYTRUE A I (ADD1 J))), which simplifies, rewriting with ARRAYTRUE-VOID-RULE and SUB1-ADD1, and opening up ARRAYTRUE and LESSP, to the following eight new conjectures: ... That finishes the proof of *1. Q.E.D. "arraytrue" is defined recursively: (DEFN arraytrue (A I J) (IF (LESSP J I) T -- the null case is true (AND (EQUAL (alltrue (selecta A I)) T) -- next element is true (arraytrue A (ADD1 I) J))) -- and rest of array is alltrue And yes, there's a machine proof that this terminates.
  - catnaroek 9y ago
    > defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) is a theorem. (proof) Sure. My point is just that a theorem is a proposition equipped with a proof. If the user just enters a proposition into the system, then they aren't entering a theorem. They're entering a proposition that the system can turn into a theorem.
- kbenson 9y ago
  > > But you'd rather prove it once so the run-time checks are unnecessary. > No. I'd rather prove it to rule out the program being wrong. The runtime check is totally besides the point. That's the same thing. It's just a matter of it being automated. > > Think of proof support as being an extension to optimization of assertions. > I never use runtime-checked assertions, so I never need to optimize them away. If you've ever used a language that uses bounds checked array access, you have. IIRC, you've used Rust some, so you've used bounds checked array access, except where Rust was able to prove that out of bounds access was impossible and elide the code that checks. > > Users need never see those proofs. > But, you see, I want to see the proofs. How am I supposed to maintain a program I don't understand? There's a difference between need and ability. Just because it's stated you don't need to see something doesn't mean you can't. If you want to see a proof, you dig in and find it, or find where it's accepted canon that we don't need to reproduce (do we need proofs for integer addition? That seems of limited use to me, but maybe a formally proved as much as possible all the way to that level language has some interesting benefits).