[racket] I love TR

On Thu, Sep 20, 2012 at 4:40 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> If these people were serious, they would add a row with industrial impact measured in $100Ms, but that would make their proof assistants look bad because ACL2's value is more than an order of magnitude the addition of all others.

Carl should add it.

> If these people were serious, Xanadu would get a lot more play. From what I can tell, it is a dependently typed language that worked. (But yes, it has been abandoned.)

Isn't ATS really Xanadu 2.0?

Jay

-- 
Jay McCarthy <jay at cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93