HtDP in Coq? Hadn't thought of of that before...
On Wed, Nov 10, 2010 at 1:26 PM, Matthias Felleisen <matth...@ccs.neu.edu> wrote: > > A factor of 2.+. > > (We could provide a type system, take away recursion, and replace it with a > structural induction form. It would be impossible to write infinite loops.) > > > On Nov 10, 2010, at 12:41 PM, John Clements wrote: > >> >> On Nov 10, 2010, at 6:50 AM, Matthias Felleisen wrote: >> >>> >>> Your reasoning is correct. What's the performance hit? >> >> In order to try it, I used the legendary 12.4.2, and... uh, it seg faulted. >> >> Okay, I submitted a bug report on that. Moving right along: >> >> Testing in the simplest way, here's what I got for permute of size 9: >> >> >> Debugging enabled, no loop protection: >> cpu time: 2520 real time: 2539 gc time: 1554 >> cpu time: 1504 real time: 1523 gc time: 542 >> cpu time: 1515 real time: 1534 gc time: 552 >> >> Debugging enabled, with loop protection: >> cpu time: 4496 real time: 4532 gc time: 1940 >> cpu time: 3653 real time: 3694 gc time: 1079 >> cpu time: 3692 real time: 3730 gc time: 1112 >> >> Debugging disabled, no loop protection: >> cpu time: 2181 real time: 2200 gc time: 1651 >> cpu time: 1132 real time: 1152 gc time: 597 >> cpu time: 1143 real time: 1163 gc time: 603 >> >> Debugging disabled, with loop protection: >> cpu time: 3458 real time: 3494 gc time: 2007 >> cpu time: 2434 real time: 2471 gc time: 972 >> cpu time: 2424 real time: 2461 gc time: 1001 >> >> ... so it's quite a bit slower. Note that a whole bunch of this slowdown in >> the "debugging enabled" category is presumably due to the errortrace >> annotation of the macro expansion. I'm guessing that folding this into the >> errortrace expansion would reduce its overhead quite a bit. >> >> John >> > > _________________________________________________ > For list-related administrative tasks: > http://lists.racket-lang.org/listinfo/dev > _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
