On Thu, Sep 20, 2012 at 4:40 PM, Matthias Felleisen <matth...@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 <j...@cs.byu.edu> Assistant Professor / Brigham Young University http://faculty.cs.byu.edu/~jay "The glory of God is Intelligence" - D&C 93 ____________________ Racket Users list: http://lists.racket-lang.org/users
