[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

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