https://terrytao.wordpress.com/career-advice/there%E2%80%99s-more-to-mathematics-than-rigour-and-proofs/
One can roughly divide mathematical education into three stages:
- The “pre-rigorous” stage, in which mathematics is taught in an
informal, intuitive manner, based on examples, fuzzy notions, and
hand-waving. (For instance, calculus is usually first introduced in
terms of slopes, areas, rates of change, and so forth.) The emphasis is
more on computation than on theory. This stage generally lasts until the
early undergraduate years.
- The “rigorous” stage, in which one is now taught that in order to do
maths “properly”, one needs to work and think in a much more precise
and formal manner (e.g. re-doing calculus by using epsilons and deltas
all over the place). The emphasis is now primarily on theory; and one is
expected to be able to comfortably manipulate abstract mathematical
objects without focusing too much on what such objects actually “mean”.
This stage usually occupies the later undergraduate and early graduate
years.
- The “post-rigorous” stage, in which one has grown comfortable with
all the rigorous foundations of one’s chosen field, and is now ready to
revisit and refine one’s pre-rigorous intuition on the subject, but this
time with the intuition solidly buttressed by rigorous theory. (For
instance, in this stage one would be able to quickly and accurately
perform computations in vector calculus by using analogies with scalar
calculus, or informal and semi-rigorous use of infinitesimals, big-O
notation, and so forth, and be able to convert all such calculations
into a rigorous argument whenever required.) The emphasis is now on
applications, intuition, and the “big picture”. This stage usually
occupies the late graduate years and beyond.
I'm of the opinion that computational mathematics is at the first stage. We write
code that "sort-of works" and lacks any attempt at formality, even failing to
provide literature references. Moving to stage 2 will be a long and tedious
task. Axiom has the connections to the proof machinery and is being
decorated to provide some early attempts at proofs using ACL2 and COQ.
This effort is an interesting combination of mathematical proof and
computational proof since both fields underlie the implementation.
Moving computational mathematics up Tao's tower is going to be a long, slow,
painul effort but, if memory serves me correctly, so was graduate school.
Tim