Re: Do people who use Ada also use ocaml or F#?

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

Le Sat, 30 Oct 2010 21:37:31 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
>> I do not see how this could be less safe than a design process itself.
>> Generics are like building something with a pattern, and this pattern is
>> checked for consistency in Ada.
>
> So are machine instructions when executed by the processor. The argument  
> is invalid: whatever does Ada with the instances of a generic body is
> irrelevant to checking the generic body.
What Ada do with generics is predictable, so you can theoretically prove  
an instantiation of a generic at some point with some parameters will  
fulfill some needs. What is different than when you re-use a method from a  
library and that library was not specifically designed for your  
application ? You have to check what you re-use is indeed the (or one of)  
the good stuff to use.

> So are machine instructions when executed by the processor.
Everything is better checked at multiple level of precisions : at the  
requirement/expectation level, at the model level, at the implementation  
design level, at the binary produced by the compiler. Real safety requires  
check up to the level of machine code (and CPU and so on), less safety  
requires less check (unless a big-bug occurs and you suspect the compiler).

If I understand you correctly, you complain you have a level to check (or  
else if what you said means “generics cannot be checked at all”, tell  
why). That is what is strange to me. Not provable, is one thing, provable  
at this stage instead of this one is another topic. Why should generic  
usage be provable before instantiation ? (you have at least a proof of  
some consistency with Ada, even before instantiation).

> whatever does Ada with the instances of a generic body is irrelevant.
Why is its predictable behavior irrelevant ? Isn't it the opposite ?


-- 
Si les chats miaulent et font autant de vocalises bizarres, c’est pas pour  
les chiens.