It sounds to be wasting a lot of time proving things about programming, when the spirit of Lisp is usually much more test-driven and not proving things. The stated goal is so that you can go about your normal business, but PROVABLY! I'd say this is much more in the spirit of ML than the spirit of Lisp.