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

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

On Sat, 30 Oct 2010 23:53:13 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Sat, 30 Oct 2010 22:54:39 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
>>> Why should generic usage be provable before instantiation ?
>>
>> Because you want to be able to deliver generic components.
> What would be your requirements to state you are able to deliver a library  
> ? (I mean a library, as a library, not linked to an application).
> 
> Aren't generics similar to libraries ?

to macro libraries

> If you are to deliver a generic as standalone, then there are things you  
> will never be able to prove, right, but just like you will not be able to  
> prove anything for a standalone library you've delivered.

The requirement is that what cannot be proved must be testable. Generics do
not fulfill it. As for provability, note also that generics fail here not
only because normal issues of something being undecidable. The train stops
miles before. Generics lack contracts [*]. You just cannot verify the
behavior since it is not specified. The specifications of Ada generics are
generic.

-------------
* Of course Ada generics have contracts (formal generic parameters etc),
but these exist at the meta language level, useless for checks and tests.

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