# [racket] proof assistants, DrRacket and Bootstrap

To answer the first part of your email, yes. Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem prover.
-Ian
----- Original Message -----
From: Bill Richter <richter at math.northwestern.edu>
To: users at racket-lang.org
Sent: Sat, 27 Sep 2014 03:38:48 -0400 (EDT)
Subject: [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
____________________
Racket Users list:
http://lists.racket-lang.org/users