18.1 Developing certified programs: Motivations
18.1 Developing certified programs: Motivations
We want to develop certified programs automatically proved by the
system. That is to say, instead of giving a specification, an
interactive proof and then extracting a program, the user gives the
program he wants to prove and the corresponding specification. Using
this information, an automatic proof is developed which solves the
``informative'' goals without the help of the user. When the proof is
finished, the extracted program is guaranteed to be correct and
corresponds to the one given by the user. The tactic uses the fact
that the extracted program is a skeleton of its corresponding proof.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.7.0.html at 8/10/98