Glen, It is kind of funny to me, and yet should not surprise me, that an individual was motivated to write a theorem prover in R. OTOH, every attempt I have ever made to get Agda to work for me has required sandboxing my Haskell environments and switching to an emacs editor, so hey. Still, the project strikes me as being one of bull headedness, a just-to-see-if-one-can kind of thing.
Do you think they will go so far as to implement general dependent typing? Last night at some point, I was thinking about the problem of implementing flexible contravariant functors in a computing language. This often appears to a stumbling block when I set out to define *for all* and *there exists* from a substitution functor, a la Topos theory. Any thoughts are welcome. Jon
============================================================ FRIAM Applied Complexity Group listserv Meets Fridays 9a-11:30 at cafe at St. John's College to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com archives back to 2003: http://friam.471366.n2.nabble.com/ FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove
