[FRIAM] AMS Notices: A Special Issue on Formal Proof

[Owen Densmore]

A fascinating issue from the AMS  http://www.ams.org/notices/200811/

The preview:
     "Using computers in proofs both extends mathematics with new  
results and creates new mathematical questions about the nature and  
technique of such proofs. This special issue features a collection of  
articles by practitioners and theorists of such formal proofs which  
explore both aspects."

A problem a few of us have been discussing at The Complex is the  
division between computing and mathematics, between algorithms and  
equations.

For example: Is current mathematical notation today's roman numerals,  
a syntax we have to leave behind or enhance to integrate with  
algorithms or "scripts".

Fascinating folks in the past like Ken Iverson have made serious  
inroads with APL, a formalized mathematical computing language.   
(currently advanced by his son Ralph in a new, more modern form as J: http://www.jsoftware.com/)

     -- Owen