Perhaps, but as I mentioned in my last comment, formal reasoning often breaks down when dealing with anything more than the simplest of systems. What kind of axioms can you reason from in software? The network is always slow: not always, memory is always abundant, not always, the disk is always slow, with virtual memory, not always, exponential time complexity is always bad... not always. And especially, factor in cost, which is one of the most important aspects, and that severely impacts even the ability to formally reason since the most correct version can also be the most expensive and time consuming to implement..
Anyways, I didn't mean to downplay formal reasoning, but just to indicate that it is not often practical to use those methods exclusively when building software.
It makes sense to reason from the specifications of the runtime environment. For example, the spec for memcpy says that it's behavior is undefined when memory areas overlap. Then it would not be correct to use it for overlapping memory areas even if it works in some particular implementation as trial and error may show.
Anyways, I didn't mean to downplay formal reasoning, but just to indicate that it is not often practical to use those methods exclusively when building software.