[SystemSafety] Logic

[GRAZEBROOK, Alvery N]

Hi Derek,

Having followed your link to QuackWatch, I was disappointed to find a piece of rhetoric with no logical backing. What a load of waffle. I'm a supporter of following scientific method, but this piece does nothing to provide evidence against the value of logic as a tool for software engineers. 

On the original topic of Logic, to apply logic does not always require that you formally verify the logic. 
a) there are large examples of the application of formal verification to software. 
b) there are more examples of the application of logic to software specification, without full "formal verification"
c) there are also examples of software development, where the only "logic" is the implementation

I think most people on the list will agree that category c) is likely to contain a higher density of bugs than the other two. I've seen some evidence that this is generally true. 

This argument all started with a question about the need to teach logic to undergraduate Informatics students. Since the discussion of teaching logic properly applies to the practice of both categories a) and b), the need for software engineers to understand logic is clear.

There is a separate debate on how practical it is to apply formal verification to every large project (i.e. whether a) or b) is preferable for any given project). If this is the debate you wish to enter, could you change the subject line to make it clear? I am personally convinced that we need to teach logic to Informatics students regardless. 

Cheers,
	Alvery

-----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 4:10 PM
To: systemsafety at lists.techfak.uni-bielefeld.de
Subject: Re: [SystemSafety] Logic

On 18/02/2014 15:49, Martyn Thomas wrote:
> On 18/02/2014 14:36, Derek M Jones wrote:
>> 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 have seen mathematically formal methods used successfully on 
> industrial projects involving more than a hundred engineers and 
> thousands of person-days of effort. I have seen formal proofs carried

Having a few bodies in a corner office working on formal methods is small scale, just because they are part of a large project does not make the use large scale.

> out on safety-critical metro systems by industrial engineers at 
> Siemens Transportation and on the message choreographies for 
> electronic commerce systems by software engineers at SAP.

This appears to be claiming large scale application by association with large companies.

Some of the points in this article on QuackWatch provide good advice to anybody who wants to evaluate the claims of formal methods
proponents:
http://www.quackwatch.com/01QuackeryRelatedTopics/pseudo.html

> In my opinion, the larger and more complex a system is, the more it 
> requires the use of abstraction to master the complexity; abstraction 
> without formal logic is just arm-waving.

That is a rather narrow view of what abstraction is about.

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

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

This mail has originated outside your organization, either from an external partner or the Global Internet.
Keep this in mind if you answer this message.



This email (including any attachments) may contain confidential and/or privileged information or information otherwise protected from disclosure. If you are not the intended recipient please notify the sender immediately and delete this email and any attachments from your system.  Do not copy this email or any attachments and do not use it for any purpose or disclose its content to any person.  Airbus Operations Limited disclaims all liability if this email transmission has been corrupted by virus, altered or falsified.  

Airbus Operations Limited, a company registered in England and Wales, with registration number 3468788.  Registered office:  Pegasus House, Aerospace Avenue, Filton, Bristol, BS99 7AR, UK.