Re: Ada 2012 Constraints (WRT an Ada IR)

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 14/12/2016 22:46, Shark8 wrote:
> On Wednesday, December 14, 2016 at 1:04:53 PM UTC-7, Dmitry A. Kazakov wrote:

> It's relevant because it is exactly showing how to represent
> restrictions [exclusions] on values (within a set); and, as we know, a
> type is a set of values and a set of operations acting on those values.
> -- This maps directly to Ada, given the LRM's definition of subtypes.

Well, but first it is an implementation issue, as such, of a very 
secondary order to the question of constrained types and other means to 
create new types. Secondly arbitrary constraints is low level and thus a 
bad idea to introduce into the type system, as dynamic predicates 
promptly illustrate. Resemblance to Ada 83 subtypes is only superficial.

>>> In this light, integrating SPARK proving with the Ada compiler could
>>> allow for better optimizations... and if it can be done in such a way
>>> that it can be leveraged in other portions of the compiler (say semantic
>>> checks), then why not use it?
>>
>> When that comes into life, programmers surely will, though not in the
>> form of preconditions, because as I said, it is bad design. The rule is
>> weakening preconditions, strengthening post-conditions.
>
> I think you may be overestimating the group "programmers".
> Seriously, the thread "C# new features (v.7)" --
> https://groups.google.com/forum/#!topic/comp.lang.ada/mLZIo_Sjm5c --
> lists things that "modern" languages are just getting that Ada has had
> for years.

Ada programmers? Ada people are very interested in formal verification. 
The problem is integration of SPARK into Ada and arbitrary constraints 
would be only obstacle here. The lower is the level of a construct more 
difficult is verification.

> Integrating these useful technologies into the compiler in a manner
> that is invisible to users [non-implementer Ada programmers] is a good
> way to ensure that the tools are used. (e.g. the Ada compiler does
> automatically what C's Lint did, and is much better for it. [Most of the
> C programmers I knew in college *never* used lint.])

Right, because it is a tool you could use or not. In Ada type 
declarations must be there, so it is not a tool, but an integral part of 
the language. This is why "pre"-aspects is a non-starter even ignoring 
their semantic consistency issues. You can do things with or without 
them. Psychologically it won't work.

> Now, if we can also leverage these technologies to make
> implementations [of Ada] better [quality-wise] and more maintainable,
> then that's win-win all the way around at the cost of (a) designing your
> IR to be amiable to the prover-module, and (b) implementing the
> prover-module.

I am against that, see above, it must be an integral part of the Ada's 
declarative framework, never a module or a tool.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de