[FOM] Object-Oriented Formal Mathematical Languages

[steven@pearavenue.com]

In support of Tony Hoare - I worked with his group at Oxford while defining one of the languages based on his formalism CSP - that language was the Occam programming language that deals with communication and concurrency - and we were very focused on the formal verification of computer programs. 

It is only a matter of economics that lets software companies get away with the liberal informality of modern programming languages.  If the penalty for shipping faultly code was equal to the penalty in the semiconductor business (which can amount to million of dollars) then you would see software houses demanding formal practice, verification, demonstration of certain properties (such as deadlock feeedom) and proof that a program met its specification.

As it is th cost of poor practice is simply passed to the consumer.

That computer programmers are not mathematicians is matter only of economic tolerance and engineering pragmatics.

With respect,
Steven

"Dennis E. Hamilton" <dennis.hamilton at acm.org> wrote ..
> Victor Makarov, in
> <http://www.cs.nyu.edu/pipermail/fom/2004-May/008154.html>,
> states, quoting Sir Tony Hoare:
> 
> 	"Programming is a mathematical activity. Like other branches of
> 	 applied mathematics and engineering,its successful practice
> 	 requires determined and meticulous application of traditional
> 	 methods of mathematical understanding, calculation and proofs".
> 
> 	But what is mathematcal activity? It is creating new theories and
> 	writing definitions and proofs in these theories.
> 
> Based on my extensive experience of practical programming since 1958, I
> assert that this is an unfortunate over-generalization.  I see enormous
> quantities of successful practice that shows little evidence of what I
> would
> call mathematical activity.  And I do not doubt the value of a mathematical
> perspective in creation of software.
> 
> I am keenly interested in the connection between software and mathematics
> (and logic and language).  I accept that it is off-purpose for FOM and
> welcome off-list suggestions of more-appropriate forums/communities where
> the connections might be explored.
> 
>  - Dennis
>  - - - - - - - - -
> "I don't even know how to formulate the concept that a METAFONT program
> draws a beautiful letter A, so I couldn't possibly prove the correctness
> of
> such a program.  But still, somehow, the theory that I've learned while
> doing computer science gives me more confidence in the programs that I
> have
> written."  Donald E. Knuth, Things a Computer Scientist Rarely Talks About,
> pp.17-18.
> 
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom