To see it done with imperative style, check out Stavely's write-up or book on the Cleanroom method: http://infohost.nmt.edu/~al/cseet-paper.html http://infohos

To see it done with imperative style, check out Stavely's write-up or book on the Cleanroom method: http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html I'd like to see a HtDP/Racket attempt at Cleanroom to see what differences or similarities there would be. SPARK Ada and miniKanren, too. It's already closer to them with its algebraic style of specification of programs that use only a few primitives for easier analysis. Edit to add that what DonaldPShimoda describes is exactly what Cleanroom required with its "intended functions."