Re: [SystemSafety] Logic

From: Dewi Daniels < >
Date: Tue, 18 Feb 2014 17:13:13 -0000


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_xxxxxx
 
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_xxxxxx [mailto:systemsafety-bounces_at_xxxxxx Derek M Jones
Sent: 18 February 2014 14:36
To: systemsafety_at_xxxxxx 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_xxxxxx >

-- 
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_xxxxxx


_______________________________________________
The System Safety Mailing List
systemsafety_at_xxxxxx
Received on Tue Feb 18 2014 - 18:14:51 CET

This archive was generated by hypermail 2.3.0 : Sat Feb 16 2019 - 02:17:06 CET