[FOM] "Hidden" contradictions

[Steven Ericsson-Zenith]

Mathematics and mathematical logic have dealt with and contained "inconsistencies" all along - and have provided adequate means to reason about them. The inadequacies of software systems will not, it seems to me, be aided by encouraging, or resigning ourselves to, a lack of rigor or disciplined effort in that field.

The problem is not with the available calculi or method. The problem is an engineering one related to human capacity and training. 

I cite two passages from Nancy Leveson's well cited paper "The Role of Software in Spacecraft Accidents." 

"While formal and executable specification languages have tremendous potential for enhancing our ability to understand the implications of complex software behavior and to provide correct and complete requirements, most of the languages created by computer scientists require too much reviewer training to be practical. A high priority on readability and learnability has not been placed on the development of such languages."

Leveson concludes:

"We need to apply the same good engineering practices to software development that we apply to other engineering technologies while at the same time understanding the differences and making the appropriate changes to handle them. There is no magic in software—it requires hard work and is difficult to do well, ..."

From the formal systems point of view the problem is not just software. This problem would be greatly aided by, and is - in fact - dependent upon, processor and systems manufacturers provided long overdue formal specifications of their computing platforms, upon which the formal properties of software, to which proper methods have been applied, may be shown to be preserved.

Regards,
Steven 

--
	Dr. Steven Ericsson-Zenith
	Institute for Advanced Science & Engineering
	http://iase.info



On Aug 22, 2013, at 11:53 PM, Carl Hewitt <hewitt at concurrency.biz> wrote:

> Mark Steiner raised some interesting questions in his post about Wittgenstein versus Turing.
> 
> A very important point that Wittgenstein made on the subject was:  "...even at this stage, I predict a time when there will be mathematical investigations of calculi containing contradictions, and people will actually be proud of having emancipated themselves from consistency."
> 
> Today, we have such inconsistency robust (paraconsistent) calculi.  There are whole conferences devoted to the subject, e.g., Inconsistency Robustness 2011/2014 (see http://robust11.org and http://ir14.org) and there are even scientific societies (e.g. iRobust see http://irobust.org).  However, the subject is still in its infancy.
> 
> Inconsistencies are pervasive in large software systems.  Unfortunately, these inconsistencies cause "bridges to fall down" with alarming regularity.  In some cases, it has been impossible to trace back which inconsistencies caused a disaster.  See the ACM Risks Forum newsgroup moderated by Peter Neumann for an ongoing saga. Some contradictions have been discovered using subtle reasoning.
> 
> Initially attempts were made to deal with software inconsistencies in large software systems by "sweeping them under the rug" by denying that there are "real" inconsistencies.  Failing this, the following were attempted:
> * developing a procedure to prevent the introduction of inconsistencies
> * developing a procedure to systematically find and eradicate inconsistencies 
> 
> Neither of the above have been very successful in reducing the pervasiveness of inconsistencies.  Consequently, it is expected that inconsistencies will remain pervasive in large software systems.
> 
> Regards,
> Carl Hewitt
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom