Re: Ada noob here! Is Ada widely used?

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Fri, 21 May 2010 22:11:34 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> SPARK is a specialized language designed for high integrity and safety
> critical programming.
With due respect, I was just to say I don't agree with the critical  
condition which appears in all wordings talking about SPARK. This (SPARK)  
is just nice when you want to proof something works, when you want to  
proofs there will not be any runtime error or specification violation.  
Obviously, this is welcome in critical areas... while not only.

There is no need to deal with a critical area to seek for that : this may  
simply be because you want better as much as it is possible or because you  
want something to be well-done as much as it is possible. The exact same  
reasons you have to choose a typed language instead of a non-typed one.  
Many people do things, in some manner, with non-typed language. Just the  
way its done differs, and not every body have the same requirements. Some  
have requirements which makes them say they don't need typed language.  
Some don't agree with that. This depends on what the author wish.

By the way, the definition of hat a critical area is, does not seems  
clear. Some ones may say “this is critical” while some other will not.

I like to say SPARK is a step above types and declarations. This seems to  
better cover its purpose, in my humble opinion.

-- 
There is even better than a pragma Assert: a SPARK --# check.