意味論の使い道

http://www.ccs.neu.edu/home/will/Personal/Nerdliness/callcc.txt

(call/cc (lambda (c) (0 (c 1))))

は、Schemeとしては、1を返すべきというのを、Schemeの形式意味論を使って、証明しているらしい。RxRSの末尾に載ってる意味論って、何か役に立つのかと思ってたけど、こういう使い道があるのか、と感心(これを役に立ってるというのかは、微妙だけど)。さて、この証明を、形式的に検証することはできるんでしょうか