((( [logo]Racket )))Need Help?
AboutDownloadDocumentationPackagesCommunityLearning

[racket] proof assistants, DrRacket and Bootstrap

From: Bill Richter (richter at math.northwestern.edu)
Date: Sat Sep 27 18:26:44 EDT 2014		 
   ACL2 [is] probably far and away the theorem prover that has had the
   most industrial impact

Interesting, Prabhakar!  I had not heard that before.  

   A DrRacket interface to Coq or Isabelle would, in contrast, be more
   superficial, in the style of Proof General.

I think so, but interfaces are really important, and DrRacket has a beautiful interface. 

-- 
Best,
Bill
Posted on the users mailing list.