[SystemSafety] Logic

[Dewi Daniels]

Derek,

You wrote:

> Formal logic is all well and good for small systems but it does not scale.
I think you should explain this important issue to your students.

> The practical usefulness of formal logic for anything but the smallest
problem is wildly overblown in computer science and I continue to be amazed
> by the claims made by the proponents of this approach:

I think that a formal education in the theory of computing is about much
more than learning how to read and write Z specifications and construct
program proofs. The essence of engineering is the application of scientific
knowledge to solve practical problems. An understanding of the underlying
science is what distinguishes an engineer from a craftsman. I strongly
believe that I and my fellow undergraduates became better programmers
(indeed, could only have become software engineers) by being taught the
theory as well as the practice of computing, despite the fact that most of
my classmates did not go on to apply formal methods directly in their
careers.

You also wrote:

> It is also arm-waving to say that formal methods will scale to large
(i.e., more than a few hundred lines) systems.

I am astonished by this statement. I was personally involved in the program
proof of several thousand lines of code in the early 1990s, including the
Full Authority Digital Engine Controller for the Rolls-Royce RB 211-535.
Since then, there have been many much larger applications of formal methods,
including SHOLIS, Tokeneer and iFACTS. Furthermore, there has been a
noticeable reduction in the number of Blue Screens Of Death in Microsoft
Windows in the large decade; I understand this has, to a large extent, been
achieved by the adoption by Microsoft of a tool based on formal methods to
detect defects in third-party device drivers (see e.g.
http://research.microsoft.com/pubs/70038/tr-2004-08.pdf). I find your
suggestion that formal methods have not been used on programs of more than a
few hundred lines to be very surprising.

Yours,
 
Dewi Daniels | Managing Director | Verocel Limited
Direct Dial +44 1225 718912 | Mobile +44 7968 837742 |
Email ddaniels at verocel.com
 
Verocel Limited is a company registered in England and Wales. Company
number: 7407595. Registered office: Grangeside Business Support Centre, 129
Devizes Road, Hilperton, Trowbridge, United Kingdom BA14 7SZ

-----Original Message-----
From: systemsafety-bounces at lists.techfak.uni-bielefeld.de
[mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] On Behalf Of
Derek M Jones
Sent: 18 February 2014 14:36
To: systemsafety at lists.techfak.uni-bielefeld.de
Subject: Re: [SystemSafety] Logic

Peter,

> I have put a White Paper, The Importance of Logic in the Informatics 
> Curriculum, up on our WWW site at 
> http://www.rvs.uni-bielefeld.de/publications/WhitePapers/LogicInInform
> aticsCurriculum.pdf . This makes the case for studying some formal 
> language with an unambiguous semantics in general, and logic in 
> particular, in *any* informatics curriculum. It works off some key 
> observations which some of you

Formal logic is all well and good for small systems but it does not scale.
I think you should explain this important issue to your students.

A mathematicians point of view:
"Highly complex proofs and implications of such proofs"
http://rsta.royalsocietypublishing.org/content/363/1835/2401

The practical usefulness of formal logic for anything but the smallest
problem is wildly overblown in computer science and I continue to be amazed
by the claims made by the proponents of this approach:
http://shape-of-code.coding-guidelines.com/2013/03/10/verified-compilers-and
-soap-powder-advertising/

> have made, and a key intervention by Tobias Nipkow at TU München, who 
> pointed me to a paper by Joe Halpern et al on the "Unreasonable 
> Effectiveness" of logic in informatics, published in the Bulletin of 
> Symbolic Logic, following the relatively well-known line of work with this
phrase in the title by Gene Wigner and Richard Hamming, about math in the
natural sciences.
>
> I wrote this paper yesterday and today so I could tell all our 
> students to read it. A paper summarising the discussion and affidavits 
> that have appeared in this thread so far, in White Paper format, will 
> follow, contributors willing (obviously I shall ask beforehand. 
> Contributions to the List appear in the publicly-accessible archive, of
course. Some contributors have mailed me privately due to company
requirements).
>
> I think it is important to address such tropes as they arise (I also 
> know that this view is not shared by all here!). The tropes, in their 
> guise as what it is acceptable to affirm or argue in professional 
> forums, affect politically what counts as good practice in our field. 
> Both John and Martyn have addressed in this thread what should count 
> as good practice (not just best practice, but good practice) and what 
> must be present, resp. is lacking, in institutional structures 
> (including professional societies and informatics curricula) to assure 
> it. In order to sort that out, the tropes must be addressed. Those of 
> us with employment tenure who have the inclination can do so :-)
>
> PBL
>
> Prof. Peter Bernard Ladkin, Faculty of Technology, University of 
> Bielefeld, 33594 Bielefeld, Germany
> Tel+msg +49 (0)521 880 7319  www.rvs.uni-bielefeld.de
>
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
>

-- 
Derek M. Jones                  tel: +44 (0) 1252 520 667
Knowledge Software Ltd          blog:shape-of-code.coding-guidelines.com
Software analysis               http://www.knosof.co.uk
_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE