correctness vs capability constraints

1.7: pos.addx/security/correctness vs capability constraints:
. I'm awed at the complexity of Ada;
they go to great lengths to
help you ensure program correctness;
but I doubt it can be used by the public .
. I think it would be sufficient to ensure only that
module capabilities were expressable and enforceable;
eg, any routes to implied sideaffects
need to be declared by a module .
. if parameters have links to caller`space,
then lack of an out-mode declaration
should by an assurance that the param
has no sideaffects .
[1.8:
. when the users call an app,
they expect know its capability limits,
yet they may also expect dynamic updates,
which could change the set of
subprograms called by the app .
. how does the user stay updated to
implied changes in app capability limits,
when the app has been linked to
more powerful subprograms ?
( you might assume that if you can trust a subprogram,
then you can trust apps to use that subprogram;
a counter example is when a worker has
top security clearance to work with your gov,
but you can't allow that work to be
employed by foreign gov's) .]
. if a subprogram has capabilities that are
greater than the app calling it,
then the app needs to
declare these enabling subprograms,
or the app's stated capabilities need to be
a function of whatever the app links into
dynamically .
. if the app's capabilities changed since
the user's last ok,
then the ok from user or mgt
has to happen again,
else the app can't be allowed to run .