"Paul Rubin" <no.email@nospam.invalid> wrote in message 
news:87d0sj379h.fsf@nightsong.com...
> Henrik Härkönen <heharkon@gmail.com> writes:
>> And interestingly, what got me initially checking more about Ada, was
>> this Wikipedia page about Dependent Types, where "Ada 202x" was listed
>> to be supporting those:
>>
>> https://en.wikipedia.org/wiki/Dependent_type
>
> I don't think that can be right, in the sense in which that term is
> normally used.  But, I think C++ uses it to mean something different, so
> maybe Ada 202x does as well.

The Wikipedia article references "Subtype predicates" (and I would add "Type 
invariants" to that) to provide this capability. Which means the reference 
really should be to Ada 2012, since that is where those were introduced. It 
also references SPARK to get static proofs.

                                         Randy.