what is needed to move from design by contract to using a more advanced prover?

Question

In "normal" programming languages such as C++ we regularly use design by contract.

The absolute bare minimum for this is to define:

• pre-conditions (expects)
• post-conditions (ensures) &
• invariants

These are typically checked by unit tests and at run time. They do not count as proofs except perhaps for the weakest proof by construction case.

What else, if anything, is needed to go from "design by contract" to using a more advanced prover?

The first improvement we can make is to try and get the compiler to check if our assertions would hold. Now the compiler is helping with formal verification. It requires a least a minimal prover of some kind.

Design by contract is typically a very simple framework whereas something like Coq has a whole host of extra features to help its users write mathematical proofs.

What are some of these features and what do they bring to the table?

These might be basic to a user of a proof assistant but may seem novel to someone from an engineering background used to DbC but with less practical exposure to formal verification or mathematic proofs.

Is there some higher level analogue to "turing completeness" suggesting a minimal number of features a proof assistent needs? or put another way what are basic tools a mathematician would want to see (maybe just for a given branch of maths).

I asked a related question on programming langauge design https://languagedesign.stackexchange.com/questions/1436/what-options-are-there-for-adding-formal-verification-to-a-general-purpose-progr and the most popular answer so far is refinement types

Examples

The paper "can c++ be made as safe as spark?" from eschertech suggests several additional things (listed in the paper) including:

• exists
• forall
• old (to refer to a value of an expression when a function was entered)

In addition to improving our "language for proofs" there may also be aspects to how they are used.

For instance I hear "tactics" mentioned in the context of proof assistants.

Sticking with the c++ theme. The standard recently added:

• concepts aka concepts-lite

Plans to add

• contracts

are in the works. And

• 'full' concepts including concept maps and axioms

were put on hold.

Concepts and contracts elevate design by contract from something typically added via library functions to part of the language that would in theory allow the compiler to use a solver like Z3.

Example contracts syntax:

int mul(int x, int y)
  [[expects: x > 0]]         // implicit default
  [[expects default: y > 0]]
  [[ensures audit res: res > 0]]{
  return x * y;
}

For concepts see for example https://en.cppreference.com/w/cpp/language/constraints

Would this be sufficient to qualify as a prover or proof assistant?

Possibly this should be a separate question but:

Does Z3 qualify as a proof assistant?

Related:

• What is a Proof Assistant?
• What makes a proof assistant a proof assistant?

Answer 1

As I see it, there are two components to pay attention to:

1. How expressive is the language of theorems?
2. How powerful is the language of proofs?

Automatic theorem provers like Z3 restrict both of these. According to Wikipedia, "Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers", and theorems always take the form "this collection of equations is satisfiable/unsatisfiable". Z3 would be hard-pressed to even state something like "isomorphism of sets is transitive" or "the rational numbers are dense in the reals" or "this particular function on floats always numerically approximates differentiation on real-valued functions to within a certain precision". Furthermore, there is minimal ability to guide Z3's proving process: when your problem falls into its domain (and many problems do), it's easy and almost magical. When your problem doesn't, you're often sad. (Disclaimer: this is all at least second-hand information, I've used Z3 exactly once.)

A proof assistant like Coq, Lean, Agda, Isabelle/HOL, etc, is much more expressive. The language of theorems is dependent type theory or higher order logic, both of which can basically capture anything a mathematician might wish to say. The proof languages are similarly expressive: almost any formal proof strategy can be encoded, it's just a question of how much work it takes to prove something. You mention tactics, which are just programs for automating the discovery and generation of proofs, which might otherwise be too painfully verbose to write by hand.

---

So it seems like there are two questions you want answers to:

1. What is an adequately expressive language for theorems?
2. What is an adequate interface for proving these theorems?

For the first, you of course want to support quantifiers (forall, exists), logical connectives (and, or, not, implies), and all the builtin data types and operations of C++. You may also want to support abstract mathematical structures and functions (for example if you want to prove that your bignums library implements arithmetic of unbounded integers).

You may also want to support other sorts of statements about functions, for example: this function is atomic; does not write to the heap; does not allocate memory; does not have undefined behavior; does not read from uninitialized or already-freed memory; does not infinite loop; has an I/O trace satisfying this property; is deterministic; is constant-time; has this asymptotic complexity; touches only these bits of heap memory in these ways and leaves the rest untouched; requires at most this much stack and this much heap; etc.

The standard way of proving things about stateful programs is Hoare Logic, which basically formalizes the rely-guarantee paradigm and can extend it to memory, I/O trace, arbitrary logical predicates, etc. If you want to support goto, you may want to look at weakest-precondition proving, which as I understand it has better support for unstructured control flow by virtue of being in continuation-passing-style.

As far as proving goes, you can decide to go for something fully automatic like Z3, perhaps aided by sprinkling in assertions to help the prover know what should be true about intermediate states. I think F* does something like this. You could also go the way of full proof assistants, where you support arbitrarily complicated reasoning to establish the facts you claim are true.

A mix of these is also possible.

Answer 2

Would this quality as a proof assistant?

Nope. C++ is unsound meaning it's pretty easy to construct invalid (false) proofs both intentionally and accidentally.

Does Z3 qualify as a proof assistant?

Nope. Z3 is an (example of) automatic theorem prover. I.e. it either finds a proof (a satisfying assignment of variables) or not without interaction with a user. It's largely a black box that either works or not.

A proof assistant to the contrary heavily interacts or even is guided by a user while constructing a proof. Thus a user interface (starting with the language) is paramount for a proof assistant.

So in the end

what is needed to move from design by contract to using a proof assistant?

To drop Turing-completeness and embrace totality at least at the level of types and proofs. Then a very high-level and expressive language with advanced automation to interact with the assistant would be highly desired. IDE support goes without saying... :)