Leslie Lamport took a shot at solving this problem (explicitness vs 'gappiness') See his "How to write a 21st century Proof" (warning PDF) paper http://research.microsoft.com/en-us/um/people/lamport/pubs/p...