Maybe a related practice (what I do): Write actual proofs or good documentation that contains essentially proofs and combine that with Knuth's Literate programming.

For what is to be proved, try to use divide and conquor to make the whole proof consist of separate steps, each of which gets a short proof and each of those steps might become a subroutine (whatever the terminology and functionality of the programming language and environment).