I beg to differ. As software itself has grown, it's developed an enormous need for axiomatic methods because of the benefits it can confer for software reliabil

I beg to differ. As software itself has grown, it's developed an enormous need for axiomatic methods because of the benefits it can confer for software reliability. Simply, we want to prove that a program is wrong at the earliest stage possible - "intuition and physical experience" is also known as "the program failed in production." Although we've invented a number of algorithmic methods to find bugs in software, the long-term trend is to find "better axioms" to define the program against, which reduce both the code size and complexity - that's the goal otherwise known as "programming language design." We don't want people to code in 19th century fashion, because it sucks.