Second
reviewer's
review | Summary:
This paper describes RUSSELL, a new language and methodology for
combining programming and proving using Coq, whose term language
subsumes a fairly full-featured functional language. There are two
standard ways to prove properties of programs written in Coq:
(a) write the program using ordinary non-dependent types, as in an
ordinary FL, and prove the properties separately; or (b) write the
program using dependent types (so-called "strong specifications") that
encode the desired properties directly, so the the program and proof
are fully integrated. The latter approach is more concise and
elegant, but is difficult to use in practice because Coq will only
accept well-typed programs, which in this case means programs already
decorated with their corresponding proofs. RUSSELL is an extension of
the ordinary Coq term language that supports an intermediate approach,
based on the idea of predicate subtyping (as used in PVS), in which
ordinary structural types are refined by logic properties. In RUSSELL,
programs can be written using predicate subtypes (similar to approach
(b)), but are accepted by the system provided merely that they are
well-typed with respect to the underlying structural types (as in
approach (a)). The proof obligations induced by the predicate
subtypes are automatically generated as lemmas to be proved
separately. The paper introduces RUSSELL via an example application to
Hinze and Paterson's Finger Trees.
Comments:
This is very interesting work on a currently hot topic: how best to
integrate dependent types into usable programming and proving systems.
Since using strong specifications directly is very challenging for
most programmers, any attempt to ease the transition from FP to
proving is worth exploring. The simplicity of the predicate subtyping
approach is appealing, although clearly more experience will be needed
to see how well RUSSELL may work in practice.
I do have some questions about the overall approach:
- You are proposing a two-stage approach to programming and proving:
first write a program that type checks structurally; then prove the
generated obligations. But how do you see this working in an iterative
development process? For example, would you suggest testing
the program once it is entered, but before attempting the proofs?
And how stable are the generated obligations under small changes
to the program or the subtype predicates?
- In practice, one of the biggest challenges for FL programmers in
using Coq is the requirement that functions be "obviously" terminating,
and you don't address this at all -- your comments on this in Section 7.3
seem naively optimistic.
The presentation could also be improved:
* It is admirable to try to make the paper self-contained by explaining
Coq, RUSSELL, and Finger Trees all from scratch, but this is perhaps
too ambitious for a conference paper, although you make a good attempt.
Some of the later sections get very compressed (see the specific comments
for some examples). Since the real topic of this paper is RUSSELL rather
than finger trees, you should consider presenting a different, simpler
example first; then you could afford to be sketchier in your treatment
of finger trees, and more openly assume that your readers already know
the Hinze & Paterson paper.
Specific Comments:
p. 3.section 2.2.3. Sections are confusing for the non-Coq expert,
and lead you to make lots of extra comments in the text about
implicit arguments (and you could usefully make still more such
comments). So are they really important for this presentation?
p. 4, section 3.1. In the presentation of the key subset equivalence
rule, it is very confusing to *start* with the derivation of a
falsehood! By all means keep this example, but first give an example
derivation of something that induces a provable obligation.
p. 4, section 3.2, para -1: This discussion of decidability of the
order relation is probably inadequate for the Coq novice.
p. 4, section 3.3, para 2: It is unclear just what proof obligations
arise from uses of the rule in Figure 6. Please say more here.
p. 5, col. 2, line 1: "we can pattern-match on d" Do matches need
to be exhaustive, as in Coq?
p.8, col 2, bottom: "This is one of the most distinctive parts of this
work..." Then please say more about it! And please clarify the
discussion at the top of the next page on using unit types; I could
not follow it at all.
p. 11, col. 1 top. It is not clear why you need to do coercions
in these cases but not in the get_set Lemma. And could such
coercions be introduced automatically?
p. 11, section 7.3. Related Work. Can you say something about
how this work is related to Refinement types a la Pfenning, Davies,
and Dunfield ? More generally, how many of your obligations are
susceptible to fully-automated proof? (cf. also the last para of
section 6.)
* The paper is engagingly written, but there are quite a few minor
language errors (some noted below), as well as a few consistent
problems:
- You frequently "comma-splice" sentences together, rather than using
a semicolon or a period.
- You mistakenly supply the verb "permit" with an infinitive rather
than a gerund. For example, you say "permits to write"; this needs to
be "permits writing" or, perhaps more idiomatically, "permits us to
write". There are about ten examples of this in the paper.
- You are sometimes excessively informal, which can make it difficult
to be sure of your meaning. Some examples:
p. 8, text line 4: "This whole Empty business..."
p. 8, Section 4.4.1., last line of text:
"You can see the long names calling for overloading here."
p. 8, col 2, line -4 before defintion of split_node: "disturbingly
resembles".
p. 11, section 7.1, line 5: "...where it still bites."
p. 12, col. 1 line 7: "...design a system with such and such effects
built-in".
Other small points:
p. 2, col 2, para 2, sentence 1: This is awkwardly phrased. Why not
characterize which recursive definitions are *accepted* instead?
p.3 section 2.2.2, para 1. Perhaps you should show the Notation
declaration for sig P.
p. 3, col 2, Section 3, line 3 : "hinges" can't be the right word.
p. 3, col 2. Section 3, para 1, sentence -1: "However, this does
not solve..." I couldn't figure out what you were trying to say here.
p. 3, col. 2, para -1, line -3 " contrary to" -> "unlike in"
p. 3, col 2, para -1, line 3: "forgeting" -> "forgetting"
p. 4, col 1, section 3.2, line 2: "It will typecheck..." It will
typecheck only if it is structurally well-typed.
p. 6, col 1. sentence 2: "Moreover, it uses..." Please clarify that
this function is an implicit parameter, because of the section mechanism.
p. 6, col 1, para -2, line -2: "(Node a)" -> "(Node v a)".
p. 6, col. 1, last para, line 5 "same type as" -> "same type because"
p. 6, Figure 8 caption: "blank nodes" -> "circled nodes" (?)
"filled" -> "shaded" (?).
p.7, col 1, para 1. Explain that the "return" clause for describing
dependent elimination is a Coq requirement.
p. 7, section 4.3, last sentence: "this adequacy with lists will hold."
I don't understand what this is supposed to mean.
p. 7, section 4.4, definition of View_L. Please explain what 'seq' is here.
p. 7, col 2, Lemma view_L_cons, last line: "s:=st'". Please explain
this notation.
p. 7, section 4.4.1, para 1 line 5: "is just as valid as recursion on
the tree" -> "are just as valid as those defined by recursion on the tree".
p. 7, section 4.4.1, para 1 line -5: you refer to but don't define
"tree_size".
p. 7, col 2, para -3, line 3 : "statement" -> "proposition". And it would
be clearer to use "vnil <> vcons x n v" as an example; otherwise the reader
might think the proposition is ill-typed because it is not true!
p. 7, col 2, para -2: "the usual trick of heterogeneous equality." Please
give a reference for JMeq. (e.g. Conor McBride's thesis).
p. 8, col 2, line 2: "what we mean" -> "the function's specification".
p. 8, col. 2, line 4 after second display : "the paper" -> "Hinze & Paterson"
(?)
p .9, col. 2, line 1 after last display: "the original paper" -> "Hinze &
Paterson" (?)
p. 10, col. 2, line 1 after third display: "strongly specified". I believe
this
is the first time you use this Coq-ism; please define it.
p. 12, section 7.2. Please give a citation for Parent's work (already in
your references?)
p. 12, section 7.3, last sentence is incomprhensible. Who is
the second author (Letouzey or one of you?), and what does the
rest of the sentence mean?
|
|---|
Third
reviewer's
review | This paper presents a case study of "Russell" an extension to the Coq
theorem prover that supports dependently-typed programming. The paper
argues that there are two modes used when programming with rich
dependent types: first, just getting the functional program down, as
one might write it in ML or Haskell, second discharging all of the
proof obligations, which one should do interactively in Coq. Russell
is a Coq extension that automatically makes this division.
I think this paper should be accepted at ICFP.
Overall, this paper provides a nice overview to Russell through the
use of an extended case study. This paper is also timely: there is
currently a lot of interest in dependently typed programming and
dependently-typed languages, and this paper provides a somewhat
large case study of one verified program. To compare all these
languages we need case studies such as this one to be available.
This paper takes a different philosophy from most other
dependently-typed languages: instead of proving correctness in
conjunction with program development, this tool allows one to
(somewhat) delay those proofs. However, this tool does not provide
full external, post-development verification---programmers must think
about what sort of properties that are necessary for verification
should be included in their definitions. Hopefully this paper will
spark some discussion about the difference between internal/external
verification at the conference.
Complaints:
I had a hard time knowing what the main point of the paper was
supposed to be: is it that we now have a certified implementation of
Finger Trees? or is the design of Russell the focus of the paper?
Because specifications are mixed with programs, it is always difficult
to know exactly what a "certified implementation" of Finger Trees
guarantees. Is there some way to characterize this precisely? Is it
just that all of the functions are total? What other correctness
guarantees do we have? How about running-time guarantees? I would
appreciate a high-level overview of what exactly was proven about the
finger tree implementation. (I.e. we show that all operations (add,
deletion, etc.), are total and that append produces a tree with length
the sum of its two arguments.... (except the generic definition of
measure makes this property a little stronger, I guess.)
I also have a question about related work. How does using Russell
compare with other ways of dependently-typed programming in Coq? For
example, Adam Chlipala has a nice paper about using the refine tactic
on his website. (Position Paper: Thoughts on Programming with Proof
Assistants. Proceedings of the Programming Languages meets Program
Verification Workshop (PLPV'06). August 2006.)
SPECIFIC COMMENTS
"Inductive types are the algebraic datatypes of Type Theories, only
more powerful". I don't understand what you are referring to by "Type
Theories" here. Yes, they are more powerful than ADTs in ML or GADTs
in Haskell, but "Type Theory" (with capital T's) usually means
Martin-L\"of dependent type theory to me.
"In implicit arguments mode, the first two arguments become implicit
as the system knows that they will be inferable at application time
from the type of the function". Should point out that, unlike in ML or
Haskell, the inference of implicit arguments is incomplete in
Coq---sometimes arguments marked as implicit must be supplied.
2.2.3 Perhaps make the connection to functors?
hinges -> hinders
"Usually, as soon as you have prepositions appearing in the type of a
function, you will write it in Coq using tactics..." what is it? the
function? the type?
Figure 5. Why do we need both rules? Doesn't symmetry suffice? (are
they not symmetric?)
Why "dest t as p in b" instead of more familiar "let p = t in b" ?
Figure 6. Does Russell automatically generate these rules from every
inductive family definition? Are indices treated differently than
parameters? Figure 6 seems not to distinguish them, but perhaps when
programming I want vector A m == vector A n, but I don't want vector
A m == vector B n. Is that possible?
Section 4. I really do need more background on FingerTrees than what
is provided here. For example, I would like an intuitive explanation of
adding elements to the tree, before the details.
What is the motivation of 4.4? Why do we need to view FingerTrees as
lists?
The Haskell version of the code is 650 lines and the Coq version 600.
Where did those 50 lines go? How closely does the Coq definition line
up with the Haskell definition? Are line counts even a good
comparison?
Is there a way to extract a Russell program without satisfying all of
its proof obligations? This would allow more incremental development:
first write the program and then, after testing it to see if it is
what you want, prove the properties about it.
|
|---|