Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!van-bc!eosvcr!aew
From: aew@eosvcr.wimsey.bc.ca (Alan Walford)
Newsgroups: comp.object
Subject: Re: Global program state.
Message-ID: <8mq8u2w162w@eosvcr.wimsey.bc.ca>
Date: 3 Jan 91 19:29:06 GMT
Organization: Eos Systems Inc, Vancouver, B.C., Canada
Lines: 25

My feeling is that functional programming and statelessness makes
proofs of program correctness easier and even tractable.

Show the following to a mathmatician:

   x = 2
   x = 3

and he/she will say one of the statements is untrue. Show it to a programmer
and he/she would say x gets assigned 2 and then 3; x's final value is 3.

Yes, this is a silly and trivial example but I think it does fundamentally
show that allowing state in a program makes proving correctness all that
more difficult. I think the only successful work in program correctness
proving has be done in functional (ie. stateless) programming.

Since OO is not stateless I think we are a long way off from program
proofs of correctness. Is anyone doing work in this area and can give me
counter-examples to my "OO difficult to prove correct" statement ?

Alan Walford
Eos Systems Inc.

...uunet!van-bc!eosvcr!aew
aew@eosvcr.wimsey.bc.ca