[FOM] Object-Oriented Formal Mathematical Languages

[Steven Ericsson Zenith]

Members of FOM should be aware that formal methods in computer science are still seriously pursued - both in industry and in academia.  Many years of research begun by Tony Hoare continue under the fine leadership of Bill Roscoe at Oxford and Bill and others do publish materials fairly frequently.

However, the issues are no longer foundational but rather issues of practice.  When I last spoke with Tony Hoare, for example, his goals were modest.  He was evangelizing - within Microsoft - the simple inclusion of assertions in programs. From small beginnings ...

In another example, I spoke a year or two ago with Craig Mundie about the question. Craig is the CTO of Microsoft. He recognizes the necessity of formal practice but complains that the only solutions offered by the formal methods community are that they must rewrite everything. I asked if he was open to formal methods proposals that offered an incremental strategy and he said that he was. 

The bottom-line is that it is widely recognized that the practice of computer science is the practice of mathematics.  There simply is not a sufficiently broad understanding of the question, and a lot of short sightedness. So, funding has not found its way into the right hands - because to fix the problem requires spending a good deal of money up front.

In addition, we are outnumbered. There is no will to fix the problem.  The economy that exists to do testing the hard way and to provide ongoing consulting and support, and endless bug fixes and product releases drives the current poor practices - the labor required to support the "quick and dirty" practices employs a substantial portion of the technical population.

With respect,
Steven

"charles silver" <silver_1 at mindspring.com> wrote ..
> Steven wrote:
> > 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.
> 
>     I once worked for a company that produced
> dBASE clones. To develop our products, it
> was useful to look at dBASE bugs.  The company
> owning dBASE (Ashton-Tate) published 78
> pages of *known* dBASE bugs for the then
> current version--and of course, we found
> many that weren't published. The CEO of
> the company I was working for used the
> 78-page list of dBASE bugs as a kind of
> standard for determining when it would
> be acceptable for market release of our
> competing products.   (I remember being
> shocked at hearing this.  Some of the
> dBASE bugs were funny: a certain
> type of line of dBASE code would
> not run properly when the number of
> characters in the line was evenly divisible
> by four.)
> 
> Charlie Silver
> 
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom