[racket] proof assistants, DrRacket and Bootstrap

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