[racket-dev] Simple loop checking in beginner?

HtDP in Coq? Hadn't thought of of that before...

On Wed, Nov 10, 2010 at 1:26 PM, Matthias Felleisen
<matthias at 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
>