[racket] proof assistants, DrRacket and Bootstrap

[Bill Richter]

I have a few questions that might be off-topic. Are you interested in formal proofs? Have you considered adapting DrRacket to give an integrated editor for a proof assistant? The proof assistants Coq and Isabelle use jedit and ProofGeneral, which I think aren't nearly as nice as DrRacket. I actually use HOL Light, which nobody uses an integrated editor for. Here are the slides for a talk I gave at the Institut Henri Poincaré in the workshop ``Formalization of mathematics in proof assistants''
http://www.math.northwestern.edu/~richter/RichterIHPslide.pdf

HOL Light and Coq are written in OCaml, a dialect of ML, which is therefore similar to Scheme, but it has one difference that I wonder if anyone here's knows how to deal with. Scheme is well-suited for writing a Scheme interpreter, because of the quote feature. OCaml doesn't have a quote feature, so the question arises how to write an OCaml interpreter inside OCaml. That's not quite what I want to do, but if anyone could explain how to do it, I'd be grateful.

I have a 7th grade student I'm trying to teach Racket, and I'm a bit confused about Bootstrap and Program By Design. Is there any reason for my student not to just read HtDP?

--
Best,
Bill
____________________
Racket Users list:
http://lists.racket-lang.org/users

[Prabhakar Ragde]

> I have a few questions that might be off-topic. Are you interested
> in formal proofs? Have you considered adapting DrRacket to give an
> integrated editor for a proof assistant? The proof assistants Coq
> and Isabelle use jedit and ProofGeneral, which I think aren't nearly
> as nice as DrRacket. I actually use HOL Light, which nobody uses an
> integrated editor for. Here are the slides for a talk I gave at the

> Institut Henri Poincar? in the workshop ``Formalization of

> mathematics in proof assistants''
> http://www.math.northwestern.edu/~richter/RichterIHPslide.pdf

I am teaching a grad course using Coq right now, and using Proof General
within Emacs for it. That is not bad, but I would love to have a
DrRacket interface. I know something like this is possible, because at
Brown they used DrRacket to prepare and run OCaml programs, a few years
ago. I really don't have the time to work on this, though. (And if I
did, I would first work on teaching language subsets of Haskell, which I
also would like to have inside DrRacket.)

> HOL Light and Coq are written in OCaml, a dialect of ML, which is
> therefore similar to Scheme, but it has one difference that I wonder
> if anyone here's knows how to deal with. Scheme is well-suited for
> writing a Scheme interpreter, because of the quote feature. OCaml
> doesn't have a quote feature, so the question arises how to write an
> OCaml interpreter inside OCaml. That's not quite what I want to do,
> but if anyone could explain how to do it, I'd be grateful.

In my senior undergraduate programming language course, I have them
write various interpreters and typecheckers in various languages,
including Racket, OCaml, and Haskell. In the latter two, you need to use
algebraic datatypes to build an abstract syntax tree, and interpret
that. So the expression (* (+ 1 2) (- 3 4)) might become

(Mult (Plus (Num 1) (Num 2)) (Minus (Num 3) (Num 4)))

Writing an interpreter for such an AST is even easier than in
Racket/Scheme, due to concise pattern-matching syntax. But parsing an
expression written in faux OCaml/Haskell is quite complicated. I don't
ask students to do that, since it really is part of a separate course
(both languages come with general parsing tools that can be used).
Parsing is much easier in Racket/Scheme because of the similarity of
code/data and the presence of 'read'.

> I have a 7th grade student I'm trying to teach Racket, and I'm a bit
> confused about Bootstrap and Program By Design. Is there any reason
> for my student not to just read HtDP?

You should view word from the authors/developers as definitive, but I
would say that if your student has good algebraic skills, then using
HtDP/2e is the right path. If not, Bootstrap may be a way to help
develop those skills. --PR

[J. Ian Johnson]

To answer the first part of your email, yes. Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem prover.
-Ian

[Bill Richter]

Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem prover.

Thanks, Ian! May I suggest that you try to handle Coq, Isabelle or HOL Light? I believe these are the foremost proof assistants. The fields medalist Vladimir Voevodsky uses Coq, in which the 4-color theorem and the Feit-Thompson theorem was formalized by Georges Gonthier. Tom Hales just finished formalizing his proof of Kepler conjecture in HOL Light and Isabelle (which is HOL as well). I'm no expert, but I think that ACL2 (also Prover9) is an FOL prover, and the bulk of activity in formal proofs uses type theories. HOL is simple, it's Church's simple types (a version of the Lambda Calculus), and Coq uses a much more complicated type theory.

[Bill Richter]

Thanks, Prabhakar, this is exactly what I wanted, and you know something about it (I was barely able to install Coq):

I am teaching a grad course using Coq right now, and using Proof
General within Emacs for it. That is not bad, but I would love to
have a DrRacket interface.

> OCaml doesn't have a quote feature, so the question arises how to
> write an OCaml interpreter inside OCaml.

In my senior undergraduate programming language course, I have them
write various interpreters and typecheckers in various languages,
including Racket, OCaml, and Haskell.

[...]

I know this is way off-topic, but it seems to me that Schemers are the only people who want an elegant solution here:

But parsing an expression written in faux OCaml/Haskell is quite

complicated. [...] Parsing is much easier in Racket/Scheme because

of the similarity of code/data and the presence of 'read'.

I think it's a parsing question I'm stuck on. I think I need to use camlp to avoid the following hack/kludge which I learned from the HOL Light experts, found in my file
hol_light/RichterHilbertAxiomGeometry/readable.ml
which is part of the HOL Light distribution:

(* From update_database.ml: Execute any OCaml expression given as a string. *)

let exec = ignore o Toploop.execute_phrase false Format.std_formatter
o !Toploop.parse_toplevel_phrase o Lexing.from_string;;

(* Following miz3.ml, exec_thm returns the theorem representing a string, so *)
(* exec_thm "FORALL_PAIR_THM";; returns *)
(* val it : thm = |- !P. (!p. P p) <=> (!p1 p2. P (p1,p2)) *)

let thm_ref = ref TRUTH;;

let exec_thm s =
if Str.string_match (Str.regexp "[^;]*;") s 0 then raise Noparse
else
try exec ("thm_ref := (("^ s ^"): thm);;");
!thm_ref
with _ -> raise Noparse;;

When I posted my question on the OCaml list, the experts said don't ever use Obj.magic, but I think they didn't think much of me using Toploop either.

--
Best,
Bill

[Prabhakar Ragde]

Bill Richter wrote:

> >Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem
> >prover.
>
> Thanks, Ian! May I suggest that you try to handle Coq, Isabelle or
> HOL Light? I believe these are the foremost proof assistants. The
> fields medalist Vladimir Voevodsky uses Coq, in which the 4-color
> theorem and the Feit-Thompson theorem was formalized by Georges
> Gonthier. Tom Hales just finished formalizing his proof of Kepler
> conjecture in HOL Light and Isabelle (which is HOL as well). I'm no
> expert, but I think that ACL2 (also Prover9) is an FOL prover, and
> the bulk of activity in formal proofs uses type theories. HOL is
> simple, it's Church's simple types (a version of the Lambda
> Calculus), and Coq uses a much more complicated type theory.

I'm sorry, I forgot about Carl's Dracula work when composing my earlier
reply. ACL2 is more limited, but its advantage (besides being probably
far and away the theorem prover that has had the most industrial impact)
is that its language (Applicative Common Lisp, hence the acronym) is
much closer to Racket, allowing for stronger integration both with
DrRacket and into a Racket-based curriculum. A DrRacket interface to Coq
or Isabelle would, in contrast, be more superficial, in the style of
Proof General. --PR

[Bill Richter]

ACL2 [is] probably far and away the theorem prover that has had the
most industrial impact

Interesting, Prabhakar! I had not heard that before.

A DrRacket interface to Coq or Isabelle would, in contrast, be more
superficial, in the style of Proof General.

I think so, but interfaces are really important, and DrRacket has a beautiful interface.

--
Best,
Bill

[Prabhakar Ragde]

On 2014-09-27, 5:50 PM, Bill Richter wrote:
> Thanks, Prabhakar, this is exactly what I wanted, and you know something about it (I was barely able to install Coq):

I struggled with installing it also, especially since I'm using a Mac.
Racket has spoiled us in that respect.

> But parsing an expression written in faux OCaml/Haskell is quite
> complicated. [...] Parsing is much easier in Racket/Scheme because
> of the similarity of code/data and the presence of 'read'.
>
> I think it's a parsing question I'm stuck on. I think I need to use camlp to avoid the following hack/kludge which I learned from the HOL Light experts, found in my file
> hol_light/RichterHilbertAxiomGeometry/readable.ml
> which is part of the HOL Light distribution:
>
> (* From update_database.ml: Execute any OCaml expression given as a string. *)

I don't have enough practice in OCaml to grasp what your code does (and,
yes, it is way off-topic), but I do know that about once every month or
two, someone posts to this list about using 'eval' in Racket, and they
are warned not to use it unless they really know what they are doing and
have a suitable application (which is rare). That warning probably is
doubled in a statically-typed language, in which 'eval' should not even
be possible without subverting the type system (I gather this is what
you are doing). Translating the gist of suggestions to such posters, I
would say: do you really need to execute *any* expression? If not, use
OCamllex and/or OCamlyacc (maybe Menhir, or a smaller and cleaner parser
combinator library) to write a parser for your language subset, and then
write an interpreter for the resulting ASTs. --PR

[Bill Richter]

Translating the gist of suggestions to such posters, I would say:
do you really need to execute *any* expression? If not, use
OCamllex and/or OCamlyacc (maybe Menhir, or a smaller and cleaner
parser combinator library) to write a parser for your language
subset, and then write an interpreter for the resulting ASTs.

Thanks, Prabhakar! I think something like what you're saying is true. HOL Light is based on quite a lot of the OCaml parser camlp, and I've thought for a long time that I had to learn it myself.

I don't have enough practice in OCaml to grasp what your code does

I'm making a dialect ofHOL Light with different syntax by interpreting one of my programs as a string and then breaking the string up into the component pieces, but then I need this Toploop/exec hack to evaluate my variables. That sounds like the Scheme eval, and in Scheme you can solve that problem nicely with the quote feature.

--
Best,
Bill

[Matthias Felleisen]

On Sep 27, 2014, at 1:38 AM, Bill Richter wrote:

> Scheme is well-suited for writing a Scheme interpreter, because of the quote feature. OCaml doesn't have a quote feature, so the question arises how to write an OCaml interpreter inside OCaml. That's not quite what I want to do, but if anyone could explain how to do it, I'd be grateful.

Decouple parsing from interpreting and your ML interpreter for ML won't look too different from your Lisp/Racket/Scheme interpreter for Lisp/Racket/Scheme. Indeed, almost everyone who does the latter actually does some form of decoupling usually.

In general,

(1) pick a representation for your chosen programming language that is tree-oriented, call it AST
(2) pick a representation for the values that your programs may return, call it VAL
(3) design a function

interpreter : AST -> VAL

(4) for a typed language, also design a function

type_check : AST -> Boolean

In ML, you might try

type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST of int | ADD of ast * ast
type val = BASIC of int | FUNCTION of val -> val | ...

> I have a 7th grade student I'm trying to teach Racket, and I'm a bit confused about Bootstrap and Program By Design. Is there any reason for my student not to just read HtDP?

1. HtDP explains the above in a couple of sections.

2. HtDP is for college freshmen (roughly) and for high school students who have the patience to read. The occasional 7th and 8th grader work their way thru HtDP with adults who understand HtDP or learn to understand HtDP that way. The basic 7th grader will benefit from the material at bootstrap-world.org, which is what we use with many middle school students around the country.

-- Matthias

[Bill Richter]

type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST of int | ADD of ast * ast
type val = BASIC of int | FUNCTION of val -> val | ...

Thanks, Matthias! I know this is way off topic, but I think it's the sort of thing only Schemers understand, and I think HOL Light would be a lot better off my problem got solved. There's a lot I didn't understand with your ML explanation. Is this written down somewhere? How to write a ML interpreter in ML using your type ideas? Are you saying I don't need camlp parsing? I would find that hard to believe. Formal proofs in HOL Light are really just OCaml programs where a lot of code has already been evaluated. Here's a simple Hilbert geometry program in my dialect:

let ExistsPointOffLine = theorem `;
∀l. Line l ⇒ ∃Q. Q ∉ l

proof
intro_TAC ∀l, H1;
consider A B C such that
¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬Collinear A B C [Distinct] by fol I3;
assume (A ∈ l) ∧ (B ∈ l) ∧ (C ∈ l) [all_on] by fol ∉;
Collinear A B C [] by fol H1 - Collinear_DEF;
fol - Distinct;
qed;
`;;

I think I need the `;[...]` construct, which at present just turns my proof into a string without any backslash or newline problems, which is then passed to my function theorem. The usual HOL Light style is like this, using instead a function prove:

let MULT_0 = prove
(`!m. m * 0 = 0`,
INDUCT_TAC THEN ASM_REWRITE_TAC[MULT; ADD_CLAUSES]);;

Notice the related `[...]` construct, which I think sends the ordered pair off to heavy camlp parsing.

Thanks for the 7th and 8th advice. I think my student is smart and hard-working, and I (finally!) learned how to program reading your book HtDP, so it sounds like you're saying that I should be able to teach it to my student. I went to bootstrap-world.org and, uh, maybe I didn't look hard enough, but I didn't find anything that looked juicy.

--
Best,
Bill

[Prabhakar Ragde]

On 2014-09-28, 12:57 AM, Bill Richter wrote:

> I'm making a dialect of HOL Light with different syntax by

> interpreting one of my programs as a string and then breaking the
> string up into the component pieces, but then I need this
> Toploop/exec hack to evaluate my variables. That sounds like the
> Scheme eval, and in Scheme you can solve that problem nicely with the
> quote feature.

A Racketeer would probably tell you to use macros to define your
dialect, instead of using an eval hack. The corresponding tool for OCaml
is camlp4, and it sounds as if it would be worth your time to learn it
thoroughly. --PR

[Bill Richter]

Matthias & Prabhakar, I think I see what you're saying now. I need the camlp parser to turn my dialect-expressions into trees. Then I turn my tree into standard expressions just as one does in Scheme. The only differences is that in Scheme we have the quote function that skips the parsing step. So your ML code

MF> type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST of int | ADD of ast * ast
MF> type val = BASIC of int | FUNCTION of val -> val | ...

looks a lot like the HOL Light definition of preterms:

type preterm = Varp of string * pretype (* Variable - v *)
| Constp of string * pretype (* Constant - c *)
| Combp of preterm * preterm (* Combination - f x *)
| Absp of preterm * preterm (* Lambda-abstraction - \x. t *)
| Typing of preterm * pretype;; (* Type constraint - t : ty *)

and so we can see one of these preterms in a standard term:

# preterm_of_term `x + y`;;
val it : preterm =
Combp
(Combp
(Constp ("+",
Ptycon ("fun",
[Ptycon ("num", []);
Ptycon ("fun", [Ptycon ("num", []); Ptycon ("num", [])])])),
Varp ("x", Ptycon ("num", []))),
Varp ("y", Ptycon ("num", [])))

So the Scheme story works fine except that I haven't understood camlp or how HOL Light turns expressions `[...]` into preterms. But I feel better about investing the time into learning camlp now that I see the Scheme story remains intact in HOL Light. And you're right about my ignorance:

MF> 1. HtDP explains the above in a couple of sections.

Right, there's something I seem not to have understood in either Scheme or ML, how when we create and evaluate our trees we retain the values of our variables. I can figure that out, and HtDP sounds like a good place to start.

PR> A Racketeer would probably tell you to use macros to define your
PR> dialect, instead of using an eval hack. The corresponding tool for
PR> OCaml is camlp4, and it sounds as if it would be worth your time
PR> to learn it thoroughly.

That's an interesting comparison, and since macros, maybe I can learn to like camlp. In fact, maybe I ought to learn something about racket macros first.

--
Best,
Bill

[Bill Richter]

Matthias, I'm still thrilled with your advice about writing a ML interpreter in ML, but I think what you told me doesn't suffice, and in particular:

MF> 1. HtDP explains the above in a couple of sections.

I think HtDP only does part of the job. I think there is nothing about Scheme evaluators past Section 17.7, where you extend the 14.4 evaluator to functions:
HtDP> The goal of this section is to extend the evaluator of section
HtDP> 14.4 so that it can cope with function applications and function
HtDP> definitions.
In the Section 14.4 evaluator you don't even have variables:
http://htdp.org/2003-09-26/Book/curriculum-Z-H-19.html#node_sec_14.4
I'm sure HtDP is fine for a first course, and I profited from reading it again, but I think a better job is done in the OCaml manual, in Sec 1.7 of
http://caml.inria.fr/pub/docs/manual-ocaml/coreexamples.html
where they have something a lot like your

MF> type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST of int | ADD of ast * ast
MF> type val = BASIC of int | FUNCTION of val -> val | ...

But what I don't like is the OCaml manual's

Om> We first define a function to evaluate an expression given an
Om> environment that maps variable names to their values. For
Om> simplicity, the environment is represented as an association list.

That's fine, as long as the Scheme/ML program we're evaluating is self contained, because the only variables will be the ones we define in our program. But what if the program has free variables which are already defined? How do we get our trees to use the values in a Scheme environment already defined? I am sure you racketeers know the answer, and maybe it would be a good exercise to put in your second edition:
http://www.ccs.neu.edu/home/matthias/HtDP2e/
All I can guess is that is Sec 17.7, you say that a
HtDP> the function's name [and] the parameter name [are] symbols
so probably all variables are represented in the tree as symbols, and I guess we need a function that will take these symbols and return their values given in the bigger environment.

--
Best,
Bill

[Matthias Felleisen]

Easy.

;; SchemeExpression is one of:
;; ---

;; SchemeValue is one of:
;; ---

;; Environment = [Listof [List Variable SchemeValue]]
(define base-environment
`((sin ,sin)
(cos ,cos)
(richter ,(lambda (x) (cons x '(bill))))
...))

;; SchemeExpression -> SchemeValue
(define (evaluate e)
(evaluate-in-context e base-environment)) ;; <--- This is '() in HtDP

;; SchemeExpression Environment -> SchemeValue
(define (evaluate-in-context e)
(cond
[(constant? e) ...]
...))