Re: Ada UK conference: SPARK safety: is no delivery better than 1 defect?

[Tim Rowe <spamtrap@tgrowe.plus.net>]

Michael wrote:
> "Ludovic Brenta" <ludovic@ludovic-brenta.org> wrote in message 
> news:355dc49a-3414-4883-a268-fa3bcc493e7b@o11g2000yql.googlegroups.com...
>> I read your post three times and I still can't figure out what your
>> point is.
>>
>> You claim that "iFACTS has failed as an engineering results" >
>> --
>> Ludovic Brenta.
> 
> Hi Ludovic,
> 
> Made it "CAATS" and you get what Nav Canada is reporting in its latest 
> Operation Strategic Plan. section - 08T.4, page 53.
> http://www.navcanada.ca/ContentDefinitionFiles/Publications/CorpPublications/AdditionalPublications/Ops_Strategic_Plan_2008_2011_en.pdf
[detail snipped]

You are still not making clear what you think the cause of the delays in 
these projects is (well, you seem to be saying that it's Ada + formal 
methods, but not saying in what way they are the problem). I don't know 
what CAATS is, but I have some knowledge of iFacts, and one of the 
things I know is that it very difficult indeed to define how it should 
work. It's hard to specify, and it's hard to determine whether 
algorithms are adequate. Each of those (related) issues could lead to 
delays (or even failure) that have nothing to do with the language or 
the use of formal methods. Using Ada with formal methods you can have a 
great deal of confidence that an algorithm is correctly implemented, but 
if you don't have confidence that the algorithm correctly solves your 
problem then where's the value? This is certainly an issue for 
development of complex systems, but it's not an Ada or formal methods 
issue. I don't know whether this is the actual issue with iFacts, but it 
should be enough to show that "Ada + formal methods project has 
difficulties" doesn't necessarily mean that the difficulties are with 
Ada or formal methods. If you think Ada or formal methods is causing the 
difficulty, could you clarify why you think that, and explain what the 
specific issues are?