[SystemSafety] Logic

[C. Michael Holloway]

Based on my personal experiences, training in philosophical logic (the kind 
that applies to natural language arguments) is needed more than training in 
formal logic.   There is no evidence that training in the latter helps one 
with the former, at least not that I've seen.

On 2/18/14 12:13 PM, Dewi Daniels wrote:
> 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
>>
>
> -- 
> *cMh*
>
> /... where ignorance is bliss, 'tis folly to be wise./ Thomas Gray
>
> -- 
> /*cMh*/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20140218/857bf475/attachment.html>