[SystemSafety] Logic

[Derek M Jones]

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