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 <rich...@math.northwestern.edu> To: users@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 ____________________ Racket Users list: http://lists.racket-lang.org/users
