(I'm a software developer, not a mathematician. I'm just starting to try to understand the proof world.)<p>I'm not sure about the "disdain" the authors have about "program source code". The parallel between proofs and programs seems clear, a runnable program is only one for which all functions/subroutines/methods (in other words, abstractions) have been implemented.<p>We try to structure programs so that the abstractions are as sensible as possible, with good, preferably memorable names. A well-written program is one where the higher level is short and understandable without (always) having to dive into what the used abstractions do. It is an aim we seem to share with the writers of the paper. Sure, real world might be different, but the technology allows us to write well-readable programs.<p>Other attempts like UML/flowcharts exist, but AFAIK attempting to connect these to runnable programs (i.e. make them <i>formal program sketches</i> in the sense of the proof sketches in the linked paper) has largely been a failure (correct me if I'm wrong). The idea to write the program and mark the parts that should show up in a flowchart (i.e. the inverse of what I've mostly seen talked about, program generation from UML), to get a "human readable" version of the program, might be a new one. Maybe if mathematicians succeed with that, it would be as applicable to software engineering?<p>In any case, am I correct in saying that the envisioned aim is the same? Does mathematics have peculiarities that make the situation different (other than, perhaps, mathematicians generally not being used to "programming", or fully formalizing something)? Is this a "teething" stage in mathematics like UML was in software engineering and will largely be superseded by just "structuring programs/proofs well", which entails creating "nice libraries"?<p>PS. I have ignored that the paper is from 2003 (about the time of UML's heyday, incidentally). What has happend to the idea of proof sketches in the mean time? Is this what "tactics" is about?