http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM7CarretteWG211/M7Carrette - Revision history2026-04-05T21:08:58ZRevision history for this page on the wikiMediaWiki 1.43.5http://mw.hh.se/wg211/index.php?title=WG211/M7Carrette&diff=223&oldid=prevAdmin: 1 revision2011-12-12T10:06:27Z<p>1 revision</p>
<p><b>New page</b></p><div>[[Category:WG211]]<br />
<br />
<br />
<h1>Modern Mechanized Mathematics</h1><br />
<h3>Jacques Carrette</h3><br />
<br />
Doing mathematics by computer is divided into two camps: numerical analysis<br />
and symbolic computation, both with very different flavors. Strangely,<br />
symbolic computation itself has split into two: theorem proving and<br />
algebraic (exact) computation. These two have developed largely<br />
independently for the last 40 years [yes, that long]. But there is a subset<br />
of these two communities who are striving to merge these two strands. Along<br />
with William M. Farmer, we are implementing a new system which gives equal<br />
weight to proofs and computation. Unlike our communities of origin, we value<br />
both correctness and efficiency equally. We are now using modern techniques<br />
(partial evaluation, dependent types, abstract interpretation, generative<br />
programming, etc) to implement a new system.<br />
<br />
Another facet which we are actively exploring is the mismatch between the<br />
``mathematics process'' and current tool support. While most parts of the<br />
mathematics process have corresponding tools, no tool comes even close to<br />
offering a reasonable environment for ``doing mathematics''. I have two<br />
particular application areas which I use for requirements analysis: (formal)<br />
software engineering and mathematical analysis (i.e. calculus). From my<br />
experience, these are two areas where new tools could have a large impact.</div>Admin