[racket] I love TR

Yes, and ACL2 also has proof by reflection.
-Ian
----- Original Message -----
From: "John Clements" <clements at brinckerhoff.org>
To: "Carl Eastlund" <cce at ccs.neu.edu>
Cc: "users at racket-lang.org list" <users at racket-lang.org>, "Matthias Felleisen" <matthias at ccs.neu.edu>
Sent: Thursday, September 20, 2012 6:40:56 PM GMT -05:00 US/Canada Eastern
Subject: Re: [racket] I love TR


On Sep 20, 2012, at 3:35 PM, Carl Eastlund wrote:

> [possibly off-topic]
> 
> Is it weird to anyone else that the dependent type comparison table, as well as the proof assistant comparison table linked right above it, seem to assume that proof assistants and dependently typed languages are synonymous?  This assumption, for instance, makes ACL2 look absolutely terrible on the proof assistant comparison chart.  Even after I fixed it up to acknowledge that yes, ACL2 does have proof automation, thank you very much.

Yes, that struck me as very strange, as well.

John Clements


____________________
  Racket Users list:
  http://lists.racket-lang.org/users