[racket] proof assistants, DrRacket and Bootstrap

> 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