[SystemSafety] Logic

[Derek M Jones]

Alvery,

> Having followed your link to QuackWatch,

Having written a sentence I could not find the
link to the very good article covering the issue,
so I submitted a rather poor one.  I should have simply
deleted what I had already written.  I will have another go
at finding the link later.

A very relevant series of talks from this meeting:
Discussion Meeting Issue ‘The nature of mathematical proof’
http://rsta.royalsocietypublishing.org/content/363/1835.toc

in particular:
http://rsta.royalsocietypublishing.org/content/363/1835/2335.long

> 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