Pete Naur's "programming as theory building" is an excellent read on the topic. Not only on the executable code front, I've also found the type notation used in

Pete Naur's "programming as theory building" is an excellent read on the topic. Not only on the executable code front, I've also found the type notation used in Haskell to be a great modeling tool using which I can check the consistency of what I'm designing. I'm not talking Coq level proofs here - just an elegant notation that you can use on paper as effectively as in code.