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

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Sat, 30 Oct 2010 22:04:34 +0200, Yannick Duchêne (Hibou57) wrote:

> 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.

No, that is a halting problem.

> 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).

I only say that they are not testable. Testing is necessary for large scale
software design. Since you cannot separate generics from their instances,
their usefulness for software decomposition is at least questionable.

> Why should generic  
> usage be provable before instantiation ?

Because you want to be able to deliver generic components.

>> whatever does Ada with the instances of a generic body is irrelevant.

> Why is its predictable behavior irrelevant?

What is the behavior of a generic body? How would you define it? What are
the specifications of generic body, not of a given instance? How to verify
if the implementation is conformant to the specification?

The strength of generics comes from patching the source code at a very low
level. Deeper you descend less predictions could be made.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de