[plt-scheme] Semantic Effects In A Pure Language - Useful For Automated Correctness Proofs???

;in meta-language before translation (side-effects are welcome here):
;make-history! creates a history! object with local state

'(begin
   (define (make-history! . history)
     (define (obj . args)
       (if (null? args)
           history 
           (set! history (cons args history))))
     obj)
  
   (define history1! (make-history! 1))
   (define history2! (make-history! 2))
   (history1! 3)
   (history2! 3)
   (history1! 5)
   (history2! 7)
   (history1!)
   (history2!)) ;this part is valid Scheme code (run it to see what it does)

;Step One (Name Your Program):

(define P
  '(begin
     (define (make-history! . history)
       (define (obj . args)
         (if (null? args)
             history 
             (set! history (cons args history))))
       obj)
     
     (define history1! (make-history! 1))
     (define history2! (make-history! 2))
     (history1! 3)
     (history2! 3)
     (history1! 5)
     (history2! 7)
     (history1!)
     (history2!)))

;Step Two (Modify Program Text From Step One And Execute):

(define PA
  '(begin
;     (define (make-history! . history)
;       (define (obj . args)
;         (if (null? args)
;             history 
;             (set! history (cons args history))))
;       obj)
     (define history 1)
     (define (obj . args)
       (if (null? args)
           history
           (evaluate-the-next-program-carrying-along-the-value-of-history-for-what-will-be-named-PA1 (cons args history))))
     
;     (define history1! (make-history! 1))
;     (define history2! (make-history! 2))
     (obj 3)
;     (history2! 3)
     (obj 5)
;     (history2! 7)
     (obj)
;     (history2!)
     ))


;Step Three (Modify Program Text From Step One And Execute):

(define PB
  '(begin
;     (define (make-history! . history)
;       (define (obj . args)
;         (if (null? args)
;             history 
;             (set! history (cons args history))))
;       obj)
     (define history 2)
     (define (obj . args)
       (if (null? args)
           history
           (evaluate-the-next-program-carrying-along-the-value-of-history-for-what-will-be-named-PB1 (cons args history))))
     
;     (define history1! (make-history! 1))
;     (define history2! (make-history! 2))
;     (history1! 3)
     (obj 3)
;     (history1! 5)
     (obj 7)
;     (history1!)
     (obj)
     ))


;Step Four (Modify Program Text From Step Two And Execute):

(define PA1
  '(begin
;     (define (make-history! . history)
;       (define (obj . args)
;         (if (null? args)
;             history 
;             (set! history (cons args history))))
;       obj)
     (define history 3)
     (define (obj . args)
       (if (null? args)
           history
           (evaluate-the-next-program-carrying-along-the-value-of-history-for-what-will-be-named-PA2 (cons args history))))
     
;     (define history1! (make-history! 1))
;     (define history2! (make-history! 2))
;     (obj 3)
;     (history2! 3)
     (obj 5)
;     (history2! 7)
     (obj)
;     (history2!)
     ))

;Step Five (Repeat Until Finished - Recursing On Any Sub-Programs)

;Notice that the resulting program need not have mutable state!

;Does anyone have good ideas on how to deal with I/O in the program?

;Is This Useful? Automated Correctness Proofs In A Stateful Language???