[FOM] What is a proof?

[Robert L Knighten]

mario writes:
 > 
 > On John McCarthy wrote:
 > > 2. Formal program verification and hardware verification have been
 > > used for many years, especially since the Intel floating point
 > > division catastrophe.
 > 
 > I would like to read a couple of clear, updated primers about such work.

Formal verification of both programs and hardware has many aspects, but a good
place to start looking at the work using formal theorem proving and computer
proof assistants and particularly the verification of floating point hardware
is in the work of John Harrison at Intel.  A good overview is:

@article{Harrison2003,
author = {John Harrison},
title = {Formal Verification at Intel},
journal ={Logic in Computer Science, Symposium on},
year = {2003},
issn = {1043-6871},
pages = {45},
doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2003.1210044},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
see also http://www.cl.cam.ac.uk/~jrh13/slides/nijmegen-21jun02/slides.pdf 

And a great deal more information can be found in John's papers collected at
http://www.cl.cam.ac.uk/~jrh13/compapers.html

-- Bob

-- 
Robert L. Knighten
RLK at knighten.org