Your first paragraph
totally resonated. I've been thinking about this problem for several years. However, my approach is diametrically opposed to yours. I think our problems in software all stem from focussing on the code as the tangible artifact to maintain control over. We should instead be focusing on the
space of possible inputs that the code is intended to work for. This is something you can't deduce from the code (and automatically using the computer to deduce it, well forget about it), it requires cooperation with the original author to present things in a way that makes the state space more explicit. This is why I love projects with lots of tests. I can't be bothered to analyze static code structure, either manually (what people call 'reading'[1]) or automatically. Just show me how the program is supposed to run in all the different situations that you've considered. Let me change it and rerun the tests to find out if I broke something.
Modern programming practice emphasizes tests, which is great. However, not all kinds of tests can be written so far. So we end up doing manual certification work everytime we release or publish a new version of software, for performance, fault tolerance, etc. I want to make it all automatic. Some links about my project in case you'd like to learn more: http://akkartik.name/about; http://github.com/akkartik/mu#readme. I'd love to hear your thoughts, either here or over email (address in profile).
[1] http://akkartik.name/post/readable-bad