[bitc-dev] bitc and call/cc

[Swaroop Sridhar]

Should Bitc consider reifying continuations?
I know that a decision to not do so was taken late last year, but the 
reason I am reopening this issue is that it may be helpful in the logic 
language to write assembly-like code that is well typed.

For example, consider:

If we HAVE to write the following sequence in assembly for performance 
reasons,

     mov $0, %ecx	
f1:
     inc %ecx
     ...
	
f3: add %eax, %ebx
     cmp %ebx, 0
     je  f1
     jmp f2
     ...
     ...	

f2:
     dec %ecx
     ...

This sequence has no privileged instructions, but uses ad hoc control 
transfer. The original idea was to present the logic system with a stub, 
or a high-level equivalent of such a sequence. However, if we use 
call/cc, it might be possible to prove properties about code sequences 
that "look" very much like the above assembly language sequence.

(define seq
   (begin
    (call/cc (lambda m
      (let f1:(cont ()) (mutable m)                            ;; **1
        (call/cc (lambda k (begin (set! ecx 0) (set! f1 k))))
        (set! ecx (+ ecx 1))
        ...
        (call/cc (lambda f2
          (begin                                               ;; **2
            (set! ebx (+ eax ebx))
            (if (== ebx 0) (throw f1 ()) (throw f2 ())))
            ...
            ... ))
        (set! ecx (- %ecx 1))
        ...
       )
    ))
  )
)

**1 The only reason to annotate f1 with its type is to ward off any 
concerns about value restriction
**2 I am not capturing f3 for simplicity as it is never thrown.

The second code fragment achieves the same effect as the first, but is 
fully typed (barring any errors I may have made), and we can have some 
hope that the control flow can be tracked by the verification engine.

However, very soon, one will write:

(begin
   (call/cc (lambda k (set! f1 k)))
   (f1 ())
)

And, I am not sure whether the proof system will reach a fix point 
without itself looping for ever in this case.

Swaroop.