The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

"Savi Maharaj" writes:
 > 
 > I am playing around with the "Correctness" tactic and would like some
 > more information about the types that I am allowed to use in annotated
 > programs. My impression is that, according to the manual (Section
 > 16.2.2) any cic_term may be used as a type. 

Yes, indeed.

 > However, the syntax of
 > expressions (Fig 16.1) is much more limited. So, for example, I can
 > introduce a variable l of type "list nat", but I cannot then write
 > expressions such as "head l", so what I can actually do with l is
 > very limited.

Any  call to  a pure  function  is allowed  in an  expression, and  it
includes  any Coq function  such as  head. Therefore  "(head l")  is a
valid  expression.  But note  that  parentheses  are mandatory  around
function calls; this may explain the syntax error...

I take  this opportunity  to mention the  availability of a  new tool,
called Why,  to certify imperative  programs with Coq,  which strictly
subsumes the Correctness tactic. You'll find it at

       http://why.lri.fr

together with many examples (a  little more than those developped with
Correctness). In particular,  this tool includes weakest preconditions
computations when  intermediate annotations  are missing (this  is not
done by Correctness).

Best regards,
-- 
Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)