Re: High-Integrity OO and controlled types

[Cyrille <comar@eu.adacore.com>]

On May 2, 9:25 pm, Maciej Sobczak <see.my.homep...@gmail.com> wrote:
>
> Excluding controlled types altogether sounded like throwing baby out
> with the water, but now the motivations are a bit more clear to me.
>

HI profiles are usually much more constrained. The first goal of this
document is to gather the necessary information to make it possible to
build a safety case when using tagged types and more generally OOP in
a HI context. Usually those are banned along with almost all the
"advanced" features of the language. So no baby thrown with the water.
This is a the other way around: we put more water in the bath so that
maybe one day we can consider bathing your "controlled" baby ;-)

Once tagged types and their additional verification activities are
accepted, adding "controlled" types to the mix doesn't require a major
step forward and becomes mostly a matter of cost since there would be
additional runtime to certify and a more complex source to object
traceability.