Python from Wise Guy's Viewpoint

[prunesquallor at comcast.net]

Matthias Blume <find at my.address.elsewhere> writes:

> In fact, you should never need to "solve the halting problem" in order
> to statically check you program.  After all, the programmer *already
> has a proof* in her mind when she writes the code!  All that's needed
> (:-) is for her to provide enough hints as to what that proof is so
> that the compiler can verify it.  (The smiley is there because, as we
> are all poinfully aware of, this is much easier said than done.)


I'm having trouble proving that MYSTERY returns T for lists of finite
length.  I an idea that it would but now I'm not sure.  Can the
compiler verify it?

(defun kernel (s i)
  (list (not (car s))
	(if (car s)
	    (cadr s)
	  (cons i (cadr s)))
	(cons 'y (cons i (cons 'z (caddr s))))))

(defconstant k0 '(t () (x)))

(defun mystery (list)
  (let ((result (reduce #'kernel list :initial-value k0)))
    (cond ((null (cadr result)))
	  ((car result) (mystery (cadr result)))
	  (t (mystery (caddr result))))))