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

Reply via email to