The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 04/22/2014 03:18 AM, Gabriel Scherer wrote:
> The usual style for "code that extracts to what you expect" is to implement
> the algorithm on the plain, "weakly typed" data structure that you would
> use in ML, and prove after-the-fact that the invariants hold in a separate
> lemma. This approach produces code that is "trivially erasable", because
> after you forget about the lemmas you just have (strongly terminating) ML
> code written in Gallina syntax.
>
> If I understand correctly, you made two different, orthogonal decisions:
> 1) you encode logical invariants directly in the data-structure
> declaration: one of the indices of the "rbtree" inductive is a list of its
> elements (that is, its semantics), and the constructors expect proofs that
> this list is sorted -- and you are careful to have this proof in Prop for
> erasability
> 2) you wrote all the algorithmic content not as programs, but as proof
> scripts using tactics, so that the various functions pass as "theorems"
> whose extraction returns the initial algorithm
>
> Could you comment on why you made those choices? My (relatively limited)
> personal experience would rather indicate that (1) is not the most
> practical way to write software as of today (although it's an interesting
> design option that should be made as practical as possible by improvement
> to Gallina, in particular allowing tactic scripts as subparts of programs),
> and that (2) is a bad idea, as it makes code harder to both write and read.
>
> An argument in favor of (1) would be that, as most after-the-fact
> correctness proof in fact follow the structure of the code (or conversely
> that most implementations are performed in the order natural to also prove
> them correct), doing the implementation and the proof at the same time
> would avoid some repeated structure and thus might result in shorter
> developments. Was this a goal of your approach?

I've seen others address the difference between "classical" 
after-the-fact proofs of code and the more internal style enabled by 
dependenty-typed programming languages.  One of the arguments is as you 
suggest - after-the-fact proofs have to do considerable work just to 
follow the structure of the code.  Another reason I used this approach, 
as well as implemented functions in Coq using proof scripts, was to 
benefit from the type-checker's feedback after every implementation 
step.  In Agda and Idris, two other dependently-typed languages, that 
feedback can be experienced while using program constructs - but this is 
not (yet?) true about Coq.  I did try using Coq's Program construct, 
which allows the programmer to first establish a skeletal implementation 
using programming constructs, then respond separately to proof 
obligations it generates.  However, I could not always get Program to do 
what I wanted, and often ended up with unprovable obligations.  Also, 
use of Program removes (by design) some of the interaction with the type 
checker.

I think that the proof-script style of coding obscures what is going on 
in rbtree.v.  But, the choices of Coq (for Prop) and then proof scripts 
(for interactive type-checking-driven development of functions) were 
both very enabling in their ways.  It could even be argued that the 
unusual proof-script programming style helps to establish the point that 
once the data structures and return types are fully constrained, the 
implementation task itself doesn't need to have much attention paid to 
the algorithms being implemented, but instead can focus on the much 
smaller goals provided to the programmer by the type checker as the 
implementation of each function is incrementally built.

-- Jonathan