Re: [Spark] Arrays of Strings

[Hyman Rosen <hyrosen@mail.com>]

John R. Strohm wrote:
> When you declare an array to be of a given size, you create a proof
> obligation that the subscript expression will always be in bounds.
> Satisfying this proof obligation is what you do during verification.


Sure, I understand what program proof and verification are about.

What I'm suggesting is that there is a tension between normal Ada
usage, which is to declare your types "snugly" so that they hold
only the ranges you expect them to have, and programs which will
always be verified before they are permitted to run.