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

[Brian Drummond <brian_drummond@btconnect.com>]

On Sun, 31 Oct 2010 14:46:07 -0700 (PDT), Shark8 <onewingedshark@gmail.com>
wrote:

>On Oct 30, 1:37�pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
>wrote:

>Are generics really non-testable?
>I think they are, though perhaps they may quickly spiral into a wide
>range of tests.
>
>The simple example of a bubble-sort on an array is testable:
...
>
>Because we know that the index is a discrete type, and has the 'Pred &
>'Succ functions we can prove this to be correct; and because we are
>requiring a function "<" for the element-type we can prove that this
>is a correct and complete bubble-sort; it is also a generic function
>though.
>
>Generic
> Type Element_Type is private;

I think you have argued that it is provable, not testable!

Which, given proof tools (Spark-2025, perhaps?) is IMO more desirable, but not
quite the same thing...

Generics are still infinitely preferable to C++ templates, in which (by
instantiating them with new types) I am still finding basic compile time errors
in a well-tested example by a vastly more competent C++ programmer than I am,
years after it was first used.

- Brian