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.
;; --- 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.) On Sep 20, 2012, at 6: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. > > Carl Eastlund > > On Thu, Sep 20, 2012 at 5:57 PM, John Clements <cleme...@brinckerhoff.org> > wrote: > > On Sep 20, 2012, at 2:49 PM, Matthias Felleisen wrote: > > > > > Duplicating the row for Sage looks fine :-) > > Hope you weren't joking: > > http://en.wikipedia.org/wiki/Dependent_type#Comparison > > On a related note, someone should probably add a more prominent section on TR > in the Racket wikipedia page. Right now it gets about half a sentence…. > > John Clements > > > > > > > On Sep 20, 2012, at 5:38 PM, John Clements wrote: > > > >> > >> On Sep 20, 2012, at 2:27 PM, Matthias Felleisen wrote: > >> > >>> > >>> > >>> Are you sure that you blew your entire budget on this email? > >>> > >>> TR is a dependently typed language. While types don't entire values, they > >>> depend on those 'aspects' of values (is it a cons? is it a positive > >>> value?) that can be checked with (usually cheap) predicates. > >> > >> There's a key missing word in the second sentence of the second paragraph… > >> I think I understand what you're saying. > >> > >> Based on my tiny definition of dependent types ("types that depend on > >> values"), TR doesn't look like it has dependent types (e.g. forall n . > >> numbers less than n), but then again, staged compilation and modules may > >> throw the definition of dependent types into a cocked hat, if I can extend > >> the type system as part of an earlier phase. > >> > >> Tell me how confused I am, on a scale of 1-10 :). > >> > >> John > >> > >> PS: if TR really is dependently typed, then it should appear in the table > >> on this page: > >> > >> http://en.wikipedia.org/wiki/Dependent_type > >> > >> I'm not quite sure what you'd put for "Program Extraction", though :). > >> > >>> > >>> > >>> > >>> > >>> On Sep 20, 2012, at 5:21 PM, John Clements wrote: > >>> > >>>> … and I don't mean Teddy Roosevelt. > >>>> > >>>> TR just discovered a bug that other type systems totally wouldn't have. > >>>> As a side-benefit, it appears that TR should be able to generate > >>>> substantially faster code as a result. > >>>> > >>>> Short synopsis: > >>>> > >>>> I have inner-loop code that's using 'modulo'. As it turns out, modulo is > >>>> slow, because (among other things) it handles cases where the modulus > >>>> needs to be added or subtracted more than once. So, I wrote my own. In > >>>> fact, I specialized my own to the situation where it wrapped down only, > >>>> because it was being applied to a counter that only got bumped up by 1. > >>>> > >>>> I found another use of modulo, and pointed it to the same function. > >>>> > >>>> OOPS! the program doesn't type-check any more. Why? because TR correctly > >>>> notes that in my other use of the function, it's entirely possible for > >>>> the index to be less than zero. > >>>> > >>>> In principle, any dependent type system should have been able to figure > >>>> this out. In practice, though, I don't know of any languages that > >>>> actually support dependent types in this way… er, agda? > >>>> > >>>> Anyhow, TR just saved me a bunch of debugging time. > >>>> > >>>> Of course, I just blew it all, writing this e-mail…. > >>>> > >>>> John > >>>> > >>>> ____________________ > >>>> Racket Users list: > >>>> http://lists.racket-lang.org/users > >>> > >> > > > > > ____________________ > Racket Users list: > http://lists.racket-lang.org/users > > ____________________ Racket Users list: http://lists.racket-lang.org/users
