CVS difference for ai12s/ai12-0079-2.txt
--- ai12s/ai12-0079-2.txt 2020/01/14 02:42:17 1.2
+++ ai12s/ai12-0079-2.txt 2020/02/11 06:26:37 1.3
@@ -61,7 +61,7 @@
!proposal
** TBD. Similar to AI12-0079-1 and it's later fixups (AI12-0240-6 [overriding],
-AI12-0303-1, AI12-0310-1, and AI12-0334-2), but with some in the core
+AI12-0303-1, AI12-0310-1, and AI12-0334-2), but with some in the core
and some in an annex.
!wording
@@ -80,7 +80,7 @@
The syntax for the aspect_definition used to define a Global
aspect is as follows:
- global_aspect_definition ::=
+ global_aspect_definition ::=
NULL
| Unspecified
| global_group_designator
@@ -89,9 +89,9 @@
| extended_global_aspect_definition -- see H.7
global_aspect_element ::=
- global_mode global_set
+ global_mode global_set
| extended_global_aspect_element -- see H.7
-
+
global_mode ::=
[ OVERRIDING ] basic_global_mode
| implementation_defined_mode
@@ -99,13 +99,13 @@
basic_global_mode ::= IN | IN OUT | OUT
global_set ::= global_designator {, global_designator}
-
- global_designator ::= global_group_designator | global_name
+
+ global_designator ::= global_group_designator | global_name
global_group_designator ::= ALL | SYNCHRONIZED | ALIASED
+
+ global_name ::= /object_/name | /package_/name
- global_name ::= /object_/name | /package_/name
-
The Global aspect identifies the set of variables (which, for
the purposes of this clause includes all constants with some
part being immutably limited, or of a controlled type, private
@@ -176,7 +176,7 @@
indicates that the specification is overriding the mode of a formal
parameter with another mode to reflect the overall effect of an
invocation of the callable entity on the state associated with the
-corresponding actual parameter.
+corresponding actual parameter.
An implementation-defined global_mode may be specified, which limits the
use of the global objects to which it applies according to an
@@ -188,14 +188,14 @@
A global_set identifies a global variable set as follows:
* ALL identifies the set of all global variables;
-
+
* ALIASED identifies the set of all aliased variables, which
includes any dereference of a value of an access-to-object type;
-
+
* SYNCHRONIZED identifies the set of all synchronized variables (see 9.10),
as well as variables of a composite type all of whose
non-discriminant subcomponents are synchronized;
-
+
* global_name{, global_name} identifies the union of the sets of
variables identified by the global_names in the list, for the
following forms of global_name:
@@ -207,7 +207,7 @@
the variable parts associated with the specified formal parameter
whose parameter mode is being overridden;
- + /package_/name identifies the set of all variables declared in the
+ + /package_/name identifies the set of all variables declared in the
private part or body of the package or of a descendant
of the package, or anywhere within a private descendant
of the package.
@@ -266,7 +266,7 @@
treated somewhat like IN T. There is no burden to mention the
dereference of an access parameter in the Global aspect, as the
effects of the dereference are presumed at the call site, just like
- the effects on “normal” parameters.
+ the effects on "normal" parameters.
* if a function returns an object of a type for which the
Implicit_Dereference aspect is True (see 4.1.5), or an object of an
@@ -295,7 +295,7 @@
dereferences (such as those associated with a rename of a call, or
an allocated result of a call) are not included — they have to be
covered in the Global or Global'Class aspect in the normal way.
-
+
* if an object of a pool-specific access-to-object type is dereferenced
within an operation, and the dereference would violate the
restrictions inherent in a Global aspect applicable to the
@@ -306,13 +306,13 @@
+ the dereferenced object:
* is a part of a formal parameter of the operation whose mode
(after any overriding) would allow the operation performed on
- the dereference;
+ the dereference;
* is a part of a dereference of an object that satisfies these
same circumstances; or
* is a local object of the operation all of whose
assignments are from an object that satisfies these
- same circumstances.
-
+ same circumstances.
+
AARM Ramification: This exemption of Global checks for dereferences of
pool-specific access-to-object values is intended to allow the
typical case where a private type uses multiple objects connected
@@ -332,7 +332,7 @@
identified by the corresponding mode, or by the IN OUT mode, of the
Global'Class aspect of a corresponding dispatching subprogram of any
ancestor of T, unless the aspect of that ancestor is Unspecified.
-
+
Implementation Permissions
For a call on a subprogram that has a Global aspect that indicates that
@@ -396,11 +396,11 @@
AARM Reason: This is intended to allow preexisting usages from SPARK
2014 to remain acceptable in conforming implementations, as well as to
- provide flexibility for future enhancements. Note the word “extend” in
+ provide flexibility for future enhancements. Note the word "extend" in
this permission; we expect that any aspect usage that conforms with
the (other) rules of this clause will be accepted by any Ada
implementation, regardless of any implementation-defined extensions.
-
+
NOTES
7 For an example of the use of these aspects and attributes, see the
@@ -415,13 +415,13 @@
either explicitly or by default. No library-level entity shall
have a Global'Class aspect of Unspecified, explicitly or by
default, if it is used as part of a dispatching call.
-
+
AARM Ramification: Global'Class need not be specified on
an operation if there are no dispatching calls to the
operation, or if all of the dispatching calls are covered
by dispatching_operation_specifiers for operations
with such calls (see H.7).
-
+
Add the following section:
H.7 Extensions to Global and Global'Class Aspects
@@ -439,32 +439,32 @@
extended_global_aspect_definition ::=
USE formal_parameter_designator
| DO dispatching_operator_specifier
-
+
extended_global_aspect_element ::=
USE formal_parameter_set
| DO dispatching_operation_set
-
+
formal_parameter_designator ::=
formal_group_designator
| formal_parameter_name
-
+
formal_parameter_set ::=
formal_group_designator
| formal_parameter_name{, formal_parameter_name}
-
+
formal_group_designator ::= NULL | ALL
-
+
formal_parameter_name ::=
/formal_/subtype_mark
| /formal_subprogram_/name
| /formal_access_to_subprogram_object_/name
-
+
dispatching_operation_set ::=
dispatching_operation_specifier{, dispatching_operation_specifier}
-
+
dispatching_operation_specifier ::=
- /dispatching_operation_/name (/object_/name)
-
+ /dispatching_operation_/name (/object_/name)
+
Name Resolution Rules
A formal_parameter_name shall resolve to statically denote a formal
@@ -534,7 +534,7 @@
be called, and the only formal objects of an anonymous
access-to-subprogram type that may be dereferenced as part of a call or
passed as the actual for an access parameter, are those included in the
-formal parameter set.
+formal parameter set.
Any dispatching call occurring within the operation that does not match
a dispatching_operation_specifier is checked using the Global'Class
@@ -595,7 +595,7 @@
The next critical new "default" is that entities declared within a
generic unit are presumed to make use of *all* generic formal parameters
associated with any enclosing generic unit, while not worrying about any
-of the possible Global effects of that usage in their Global aspect.
+of the possible Global effects of that usage in their Global aspect.
These additional effects are handled at the point of instantiation,
rather than at the point of definition of the generic, much in the same
way that "purity" of an instantiation is determined by a combination of
@@ -629,7 +629,7 @@
on the Global'Class effects, which are likely to be very pessimistic,
if specified at all.
-Some overal notes on the above:
+Some overal notes on the above:
This version of this AI was based on work done by Tuck and Claire to
reach some kind of simpler consensus position on Global. Probably the
@@ -638,10 +638,10 @@
where few if any Global specifications are required. We have coupled
that with a restriction No_Unspecified_Globals to accommodate those
users who want to impose on themselves a requirement to specify Global,
-explicitly or implicitly, at least on all library-level entities.
+explicitly or implicitly, at least on all library-level entities.
A related change was to move concerns about use of generic formals to
the point of instantiation, so operations in a "pure" generic unit can
-be (implicitly or explicitly) simply "Global => null".
+be (implicitly or explicitly) simply "Global => null".
The additions relative to the consensus report are very few, and are
justified based on a strong belief we need to ensure that even if very
@@ -662,7 +662,7 @@
special aspect specifications to make use of these exemptions. We only
require that the access type be declared in a private part or a body, and
that any dereference be reachable from a formal parameter whose
-parameter mode allows for the operation performed on the dereference.
+parameter mode allows for the operation performed on the dereference.
This meets the expressed goal that existing code that "does the right
thing" as far as using access types for implementing abstract data types
does not need any additional aspect specifications and can still specify
@@ -694,5 +694,1811 @@
correctly enforced.
!appendix
+
+From: Steve Baird
+Sent: Wednesday, October 2, 2019 1:22 PM
+
+AdaCore has reviewed the Global aspect introduced in AI12-079 and subsequently
+referenced in several other AIs (e.g., AI12-267, AI12-240, AI12-302, AI12-303,
+AI12-310) and requests that the ARG consider a substantial simplification of
+the definition of this aspect.
+
+Objections to the current proposal that were raised in AdaCore's discussion
+include:
+
+ 1) It seems too complex.
+ 2) Compatibility with SPARK seems problematic.
+ 3) It seems to be an immature proposal.
+
+Discussion of this request will be an agenda item for the upcoming meeting in
+Lexington.
+
+****************************************************************
+
+From: Jeffrey Cousins
+Sent: Wednesday, October 2, 2019 1:42 PM
+
+Another last minute objection. Do they have any alternative proposal?
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, October 2, 2019 2:19 PM
+
+The most basic alternative is to eliminate the whole concept. An intermediate
+suggestion was to revert to something such as "Global => [null | synchronized
+| all]"
+
+****************************************************************
+
+From: Steve Baird
+Sent: Wednesday, October 2, 2019 2:22 PM
+
+> Do they have any alternative proposal?
+
+No, but two of the alternatives that have been discussed internally at
+AdaCore are
+ - completely eliminate the Global aspect and all uses thereof
+ from the Ada 202x language definition;
+ - disallow Global aspect specifications that specify a set
+ of referenced objects other than (roughly speaking)
+ "no objects", "all objects", or "all synchronized objects".
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Wednesday, October 2, 2019 3:47 PM
+
+> The most basic alternative is to eliminate the whole concept. An
+> intermediate suggestion was to revert to something such as
+> "Global => [null | synchronized | all]"
+
+What would be the use of "Global => all"? We suggested either "Global => null"
+or "Global => synchronized", but I don't see a use for "Global => all"? Unless
+it is to revert the effect of an enclosing "Global" contract, which I think
+is more confusing than helping in that case.
+
+****************************************************************
+
+From: Richard Wai
+Sent: Wednesday, October 2, 2019 3:27 PM
+
+The idea is that in full Ada, unlike SPARK, accessing global variables is not
+unusual. We also need to consider existing code. We prefer to avoid changes
+that break existing code. In SPARK, the default of Global is "null", meaning
+that no global access are allowed. This would not be an acceptable default for
+Ada, since it would break a huge amount of existing code, and make new code
+more complex to reason about.
+
+When using SPARK, the goal is to prove that the code will not raise
+exceptions, so the extra legwork required to describe the data dependencies
+is part of the cost of getting that proof. However for full Ada, having this
+requirement is far too extreme.
+
+So thus, the default of "all" means that the given entity can access any
+entity global to it, where as "null" means it is restricted to local entities
+only. The concept here is to provide a new tool which allows for the specific
+restriction of global accesses, by restricting them to task-safe objects or
+local-only objects.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, October 9, 2019 3:55 PM
+
+>What would be the use of "Global => all"? We suggested either "Global => null"
+>or "Global => synchronized", but I don't see a use for "Global => all"? Unless
+>it is to revert the effect of an enclosing "Global" contract, which I think is
+>more confusing than helping in that case.
+
+"all" is the default state for most (but not all) existing code. More
+importantly, we generally allow (for all aspects) a user to confirm that
+default state. Confirming an aspect always is useful, because it tells
+readers that the aspect is intended to have a particular value as opposed
+getting such a value by default.
+
+It seems likely that some organizations will require one or more
+specifications of Global in every compilation unit as part of their
+recommended programming style, and certainly such organizations will need to
+be able to write Global => all.
+
+Finally, note that "all" is not the default for *all* code; in particular,
+non-generic Pure packages default to "null". It's possible that some pure
+packages (those that dereference general access types) will need to use "all"
+(or some other global specification) on some operations, so being able to
+specify that will be necessary.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, October 9, 2019 4:03 PM
+
+It seems likely that in some packages, you would establish a default of
+"Synchronized" or "Null," but still have a few routines with side effects that
+are not thread safe. You would not want to penalize the whole package just
+because a couple of routines are not thread safe.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Wednesday, October 9, 2019 11:36 PM
+
+I am not convinced by that use case.
+The need for a package level default is rare enough in my experience that you
+don't need an escape mechanism. And that's also the only justification for
+that "Global => all". I'm even less convinced by Randy's explanations that the
+user may want to positively state that a subprogram can touch any global
+variables (which is not a proper specification in my opinion).
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Wednesday, October 9, 2019 11:30 PM
+
+> The idea is that in full Ada, unlike SPARK, accessing global variables is
+> not unusual. We also need to consider existing code. We prefer to avoid
+> changes that break existing code. In SPARK, the default of Global is "null",
+> meaning that no global access are allowed. This would not be an acceptable
+> default for Ada, since it would break a huge amount of existing code, and
+> make new code more complex to reason about.
+
+This is not true. There is no default in SPARK. The Global is computed by the
+tool when not provided explicitly.
+
+> When using SPARK, the goal is to prove that the code will not raise
+> exceptions, so the extra legwork required to describe the data dependencies
+> is part of the cost of getting that proof. However for full Ada, having this
+> requirement is far too extreme.
+
+I don't know why you say that. Most SPARK users these days don't use
+Global/Depends at all. Even those who use them do that very little, relying on
+automatic generation for all the contracts they don't care to specify.
+
+> So thus, the default of "all" means that the given entity can access any
+> entity global to it, where as "null" means it is restricted to local
+> entities only. The concept here is to provide a new tool which allows for
+> the specific restriction of global accesses, by restricting them to
+> task-safe objects or local-only objects.
+
+Understood. For me, "all" is the implicit default, which is why I don't see a
+need to specify it.
+
+****************************************************************
+
+From: Richard Wai
+Sent: Thursday, October 10, 2019 12:43 PM
+
+> This is not true. There is no default in SPARK. The Global is computed by
+> the tool when not provided explicitly.
+
+Fair enough, but we can't expect the Ada compiler to synthesize global
+contracts, so in effect this point is mute.
+
+> Understood. For me, "all" is the implicit default, which is why I don't see
+> a need to specify it.
+
+The Ada standard does not usually do implicit (thankfully). These things are
+usually defined clearly, and that is always better. If an aspect has a default
+value, there must be a specific value for that default.
+
+Also as Tuck mentioned, the enclosing scope might have a Global set to
+something more restrictive, which a subprogram needs to override. So if the
+package is Global => synchronized, a subprogram of the package might be
+Global => all. If there was not "all", it wouldn't be possible to make this
+override.
+
+I understand that you probably don't agree with that idea of overriding, but
+from a purely Ada perspective, it is orthogonal behaviour. It is similar to,
+say, the Assertion_Policy pragma.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, October 10, 2019 1:31 PM
+
+>> It seems likely that in some packages, you would establish a default of
+>> "Synchronized" or "Null," but still have a few routines with side effects
+>> that are not thread safe. You would not want to penalize the whole package
+>> just because a couple of routines are not thread safe.
+>
+> I am not convinced by that use case.
+> The need for a package level default is rare enough in my experience that
+> you don't need an escape mechanism.
+
+I think your SPARK experience might not be as relevant to how we envisage
+Global being used initially for Ada 202X, since we see Global in the near term
+being used as an important way to identify thread safety. For thread safety,
+the natural unit of concern is often the package where a type is defined,
+rather than the individual subprograms that represent the operations on the
+type.
+
+> And that's also the only justification for that "Global => all". I'm even
+> less convinced by Randy's explanations that the user may want to positively
+> state that a subprogram can touch any global variables (which is not a
+> proper specification in my opinion).
+
+It is a fundamental principle of aspects that one can always affirm the
+default. We have a few "golden" rules in Ada, and this is definitely one of
+them. Many (but alas, not all) of these "golden" rules are enshrined as
+"Language Design Principles" in the AARM. The principle associated with being
+able to express the default is partly captured by AARM 13.1(1.a.1/3):
+
+ "Confirming the value of an aspect should never change the semantics of the
+ aspect. Thus Size = 8 (for example) means the same thing whether it was
+ specified with a representation item or whether the compiler chose this
+ value by default."
+
+Sometimes we violate our own Principles, but when we do, there needs to be some
+strong overriding reason.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, October 10, 2019 3:28 PM
+
+>>It seems likely that in some packages, you would establish a default
+>>of "Synchronized" or "Null," but still have a few routines with side
+>>effects that are not thread safe. You would not want to penalize the
+>>whole package just because a couple of routines are not thread safe.
+
+>I am not convinced by that use case.
+>The need for a package level default is rare enough in my experience
+>that you don't need an escape mechanism.
+
+That's because SPARK doesn't try to contract generic units. The contract for a
+generic unit depends on the formal parameters, and it can be complex enough
+that it's impractical to repeat it on all of the contained operations. See the
+containers definition for an example of what I mean. (Without those complex
+contracts, all generics would have to be Global => all, which would be deadly
+to any use of libraries in parallel contexts.)
+
+>And that's also the only justification for that "Global => all". I'm
+>even less convinced by Randy's explanations that the user may want to
+>positively state that a subprogram can touch any global variables
+>(which is not a proper specification in my opinion).
+
+For SPARK, that may be true. That's why we're considering changing the name
+of the aspect to avoid any sort of conflict with SPARK. For Ada 202x, however,
+the primary use of the specification is for parallel safety, and the secondary
+uses are for optimization (much like pragma Pure, except specifiable
+everywhere). This is almost completely separate from any use that SPARK has.
+
+For instance, for checking parallel loops, we really only need to specify five
+states (ignoring generic and parameter issues for the moment): "in out all",
+"in all", "in out synchronized", "in synchronized", and "null" -- and all of
+the latter ones work with parallel loops while the first does not.
+More detail buys nothing with a loop since the items are being compared with
+themselves, so any unsynchronized global writes will always conflict with
+themselves and thus fail.
+
+More detail could help for parallel blocks and in Ada tasks, but it is much
+less clear whether parallel blocks would be used that much, and whether race
+checking between Ada tasks is really feasible.
+
+The existence or absence of parallel races is a critical part of the
+specification of a subprogram. It really should be given explicitly, just like
+constraints and parameter modes and preconditions.
+
+Not checking for parallel races is a nonstarter for me. I do not want to leave
+the field of "safe" parallelism to other languages like Rust, and I certainly
+do not want to require the use of separate tools to get any sort of safety
+(we've been saying for decades that Lint is an inadequate way to make C safe,
+why should the same logic not apply to Ada??). SPARK has to be a tool for a
+limited number of Ada users with critical needs, not something that is
+required to make Ada safe.
+
+In any case, a basic principle of Ada is that one can always *explicitly*
+specify something that happens implicitly. It would be madness to have a
+default of "all" but not be able to specify that.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, October 10, 2019 3:33 PM
+
+BTW, as discussed at the meeting, this discussion really ought to be on
+Ada-Comment so that the entire Ada community can weigh in.
+
+Of course, this thread demonstrates the problem, too, as a post about an
+outside discussion has morphed into a more detailed feature discussion. And
+it's hard to move existing threads without killing them off.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Sunday, October 13, 2019 9:27 AM
+
+> That's because SPARK doesn't try to contract generic units. The contract for
+> a generic unit depends on the formal parameters, and it can be complex
+> enough that it's impractical to repeat it on all of the contained
+> operations. See the containers definition for an example of what I mean.
+> (Without those complex contracts, all generics would have to be Global =>
+> all, which would be deadly to any use of libraries in parallel contexts.)
+
+Given that the standard containers are not thread-safe, I don't understand
+your point. What kind of use of standard containers do you envision in
+parallel contexts?
+
+The use of a package-level default is orthogonal IMO to the use of Global on
+generic units. Yes, for richer Global that take into account the globals of
+formal subprograms, one would need to be able to refer to these globals using
+something like Subp'Global. This is most likely a usage that is very specific
+to the subprograms inside the generic unit, as it depends on calling or not
+the formal subprogram, so I don't see the use for a package default here.
+Going beyond that and having contracts like Type'Global is defeating the
+purpose of specification IMO, by leading to contracts that no-one can
+understand.
+
+> For SPARK, that may be true. That's why we're considering changing the name
+> of the aspect to avoid any sort of conflict with SPARK. For Ada 202x,
+> however, the primary use of the specification is for parallel safety, and
+> the secondary uses are for optimization (much like pragma Pure, except
+> specifiable everywhere). This is almost completely separate from any use
+> that SPARK has.
+
+If that's true, the new Ada aspect has both a very narrow usage IMO, and will
+be a source of endless confusion, as we will continue to evolve the Global
+aspect in SPARK to ensure essentially the same things: detect harmful
+aliasing in both sequential and parallel contexts (this is already how Global
+is used in SPARK, which does support Ravenscar and Jorvik profiles!)
+
+> For instance, for checking parallel loops, we really only need to specify
+> five states (ignoring generic and parameter issues for the moment): "in out
+> all", "in all", "in out synchronized", "in synchronized", and "null" -- and
+> all of the latter ones work with parallel loops while the first does not.
+> More detail buys nothing with a loop since the items are being compared with
+> themselves, so any unsynchronized global writes will always conflict with
+> themselves and thus fail.
+
+Our investigations so far indicate that most real world usage of parallelism
+in loops are concerned with operating over the same large data structure in
+chunks, a use that corresponds precisely to your "in out all" above.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, October 14, 2019 8:01 AM
+
+> ...
+> Our investigations so far indicate that most real world usage of parallelism
+> in loops are concerned with operating over the same large data structure in
+> chunks, a use that corresponds precisely to your "in out all" above.
+
+So long as the large data structure is indexed by either the chunk parameter
+or the loop parameter, there is no problem, and no requirement for an "in out
+all." See 9.10.1(20/5) in latest 202X RM:
+
+"This policy includes the restrictions imposed by the
+Known_Parallel_Conflict_Checks policy, and in addition disallows a parallel
+construct from reading or updating a variable that is global to the construct,
+unless it is a synchronized object, or unless the construct is a parallel
+loop, and the global variable is a part of a component of an array denoted
+by an indexed component with at least one index expression that statically
+denotes the loop parameter of the loop_parameter_specification or the chunk
+parameter of the parallel loop."
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, October 14, 2019 9:24 AM
+
+> Given that the standard containers are not thread-safe, I don't understand
+> your point. What kind of use of standard containers do you envision in
+> parallel contexts?
+
+This issue is addressed by two AIs, AI12-0196-1 which make it clear that there
+is no conflict between container elements with different indices, and
+AI12-0111-1, which provides for "stable" containers which are by default used
+when iterating over a container, allowing the tampering checks to be performed
+only before and after the whole loop, rather than on each iteration.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, October 15, 2019 10:28 PM
+
+> Given that the standard containers are not thread-safe, I don't understand
+>your point. What kind of use of standard containers do you envision in parallel
+>contexts?
+
+As Tucker noted, we fixed many of the containers threading issues long ago.
+In addition to the AIs Tucker mentioned, the containers contract AI makes many
+of the containers operations (that don't depend on the formal parameters)
+Global => null, and assuming that the element type is appropriate, allows
+reading as well.
+
+Moreover, *any* generic package has this problem, and it would be a terrible
+idea to have two features (parallelism and generics) that cannot work together.
+
+>The use of a package-level default is orthogonal IMO to the use of Global
+>on generic units.
+
+Certainly true; package-level defaults make sense for many packages. Most OOP
+ADTs have little or no state, for instance, and thus all of the operations in
+the package ought to be declared Global => null. Reusable packages also often
+don't have state. Most language-defined packages can only have synchronized
+state (since they are supposed to be reentrant). Repeating such a declaration
+on every individual subprogram would add a lot of clutter (especially if the
+possibly optional package-level specifications are used).
+
+...
+>> For instance, for checking parallel loops, we really only need to specify
+>> five states (ignoring generic and parameter issues for the moment): "in out
+>> all", "in all", "in out synchronized", "in synchronized", and "null" -- and
+>> all of the latter ones work with parallel loops while the first does not.
+>> More detail buys nothing with a loop since the items are being compared with
+>> themselves, so any unsynchronized global writes will always conflict with
+>> themselves and thus fail.
+
+> Our investigations so far indicate that most real world usage of parallelism
+>in loops are concerned with operating over the same large data structure in
+>chunks, a use that corresponds precisely to your "in out all" above.
+
+Surely not. If the data structure is passed as a parameter (as in a
+container), then it doesn't appear in the global at all; the operation will
+often be global null. If the data structure is only being read (a quite common
+occurrence), then there is no conflict. Tucker also noted the special cases for
+writing arrays.
+
+Moreover, if Ada is to grow with the future, it has to have facilities to not
+just do the sorts of parallelism that people are writing today, but also to
+have abilities to write other sorts of uses in the future. Personally, I can
+only think of one data structure that I have *ever* written (in 40 years of
+programming) that could be parallelized by "chunking a large data structure".
+Most if the structures I've used are trees of some sort that were created
+directly with unstructured access types -- partitioning them usefully would
+take more time than you could ever gain.
+
+Ideally, it would be possible to parallelize much of that existing code
+without having to rewrite much of it (for that, SPARK is a non-starter).
+Such code is far too complex to have any hope of finding conflicts by hand;
+the compiler has to do it.
+
+Certainly, this first version isn't going to work for everyone or in every
+circumstance (what does?), but if we don't try, we'll be leaving that for
+other people to do and those will almost certainly not do the careful
+language design (for readability, correctness, and all of the other motherhood
+things) of Ada.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Wednesday, October 16, 2019 12:18 AM
+
+> As Tucker noted, we fixed many of the containers threading issues long ago.
+> In addition to the AIs Tucker mentioned, the containers contract AI makes
+> many of the containers operations (that don't depend on the formal
+> parameters) Global => null, and assuming that the element type is
+> appropriate, allows reading as well.
+
+I was talking of updating the containers. This is not thread safe. So you were
+only talking of reading a container, that's not so compelling to me.
+
+>Certainly true; package-level defaults make sense for many packages. Most
+>OOP ADTs have little or no state, for instance, and thus all of the
+>operations in the package ought to be declared Global => null. Reusable
+>packages also often don't have state. Most language-defined packages can
+>only have synchronized state (since they are supposed to be reentrant).
+>Repeating such a declaration on every individual subprogram would add a lot
+>of clutter (especially if the possibly optional package-level specifications
+>are used).
+
+Why not after all, although I would rather the language sticks to the simple
+version "null/all/synchronized" for these package defaults. Anything more
+complex seems overengineered/not useful IMO.
+
+>>Our investigations so far indicate that most real world usage of parallelism
+>>in loops are concerned with operating over the same large data structure in
+>>chunks, a use that corresponds precisely to your "in out all" above.
+
+>Surely not. If the data structure is passed as a parameter (as in a
+>container), then it doesn't appear in the global at all; the operation will
+>often be global null.
+
+sure, but the operation will still be rejected by the "safe parallelism"
+checking in Ada, that's my point.
+
+>If the data structure is only being read (a quite
+>common occurrence), then there is no conflict.
+
+Our limited experience with users wanting parallel speedup is to write to a
+collection, not only read.
+
+>Tucker also noted the special cases for writing arrays.
+
+What is that special case?
+
+>Moreover, if Ada is to grow with the future, it has to have facilities to
+>not just do the sorts of parallelism that people are writing today, but also
+>to have abilities to write other sorts of uses in the future. Personally, I
+>can only think of one data structure that I have *ever* written (in 40 years
+>of programming) that could be parallelized by "chunking a large data
+>structure". Most if the structures I've used are trees of some sort that
+>were created directly with unstructured access types -- partitioning them
+>usefully would take more time than you could ever gain.
+>
+>Ideally, it would be possible to parallelize much of that existing code
+>without having to rewrite much of it (for that, SPARK is a non-starter).
+>Such code is far too complex to have any hope of finding conflicts by hand;
+>the compiler has to do it.
+>
+>Certainly, this first version isn't going to work for everyone or in every
+>circumstance (what does?), but if we don't try, we'll be leaving that for
+>other people to do and those will almost certainly not do the careful
+>language design (for readability, correctness, and all of the other
+>motherhood things) of Ada.
+
+My view is quite the opposite. Unless you carefully plan in the language for
+practical uses, you're certain to design an unusable feature. The current
+design of Global (including compound objects, etc) fits that description IMO.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, October 16, 2019 1:14 AM
+
+...
+>My view is quite the opposite.
+
+Exactly. We can only agree to disagree. There's no point in continuing to
+talk to someone that isn't willing to consider the future - because it's only
+the future that is relevant here (Ada 2012 is good enough for the present and
+probably the next few years as well).
+
+>Unless you carefully plan in the language for practical uses, you're
+>certain to design an unusable feature.
+
+If we only worry about existing "practical" uses, we'll be two decades behind
+by the time of the next revision of Ada. We have to worry about future uses
+as well.
+
+>The current design of Global (including compound objects, etc) fits
+>that description IMO.
+
+For what it's worth, all of the (C and Fortran) examples shown during the
+OpenMP session would have passed the proposed conflict checks.
+
+Pretty much all reduction examples pass the proposed conflict checks. Those
+cover a large percentage of things that are typically parallelized.
+
+As I said, we will have to agree to disagree.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Wednesday, October 16, 2019 4:13 AM
+
+> Exactly. We can only agree to disagree. There's no point in continuing
+> to talk to someone that isn't willing to consider the future
+
+enough said, I was trying to have a technical discussion, not personal attacks.
+
+****************************************************************
+
+From: Raphael Amiard
+Sent: Wednesday, October 16, 2019 5:07 AM
+
+>>Understood. For me, "all" is the implicit default, which is why I don't see
+>>a need to specify it.
+
+>The Ada standard does not usually do implicit (thankfully). These things are
+>usually defined clearly, and that is always better. If an aspect has a
+>default value, there must be a specific value for that default.
+
+I agree with that, it's a bit like "in" mode for parameters. If the default
+is "all", then the user should still be able to specify it.
+
+****************************************************************
+
+From: Arnaud Charlet
+Sent: Wednesday, October 16, 2019 5:44 AM
+
+Makes sense to me too.
+
+****************************************************************
+
+From: Raphael Amiard
+Sent: Wednesday, October 16, 2019 5:54 AM
+
+>>Certainly, this first version isn't going to work for everyone or in every
+>>circumstance (what does?), but if we don't try, we'll be leaving that for
+>>other people to do and those will almost certainly not do the careful
+>>language design (for readability, correctness, and all of the other
+>>motherhood things) of Ada.
+
+>My view is quite the opposite. Unless you carefully plan in the language for
+>practical uses, you're certain to design an unusable feature. The current
+>design of Global (including compound objects, etc) fits that description IMO.
+
+I agree with Yannick. For me this is wishful design at best. "Planning" for
+the future when you're not sure what the future is, in terms of language
+design seems like a very bad idea, a good way to put a lot of features that
+won't be used. If your planning was wrong, this "careful language design"
+you're talking about will just be dead weight, while those other people will
+still have to conceive the solution that is actually right for them.
+
+For me, one such example in Ada is safety rules wrt. access types in general:
+Those have proved to be overly restrictive, to the point of making pool
+specific access types in Ada unusable for a variety of use cases. The result
+have just been people circumventing the "safety".
+
+I predict that's exactly what would happen in that case, if this aspect was
+to be implemented in a compiler in the first place - which is far from
+certain at this point, and that's something the ARG should bear in mind.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, October 16, 2019 8:18 AM
+
+>>As Tucker noted, we fixed many of the containers threading issues long ago.
+>>In addition to the AIs Tucker mentioned, the containers contract AI makes
+>>many of the containers operations (that don't depend on the formal
+>>parameters) Global => null, and assuming that the element type is
+>>appropriate, allows reading as well.
+
+>I was talking of updating the containers. This is not thread safe. So you
+>were only talking of reading a container, that's not so compelling to me.
+
+You are not limited to reading. As mentioned, "stable" containers are by
+default used by iterators in 202X (the "Iterator_View" -- see 5.5.2(12/5)),
+and stable containers allow replacing of existing elements, including in
+parallel for vectors of "definite" components. The iterators for the
+language-defined containers explicitly support parallel iteration, since
+their Iterate functions return "Parallel_Reversible" iterators.
+
+Reading is also very important for parallel applications, as any sort of
+reduction or more complex analysis is frequently a read-only operation on the
+container. In many cases, a large data structure is read many more times than
+it is updated. Most "big data" operations are generally reading huge data
+structures without overwriting them.
+
+...
+>>Surely not. If the data structure is passed as a parameter (as in a
+>>container), then it doesn't appear in the global at all; the operation will
+>>often be global null.
+
+>sure, but the operation will still be rejected by the "safe parallelism"
+>checking in Ada, that's my point.
+
+So long as the index is either the loop parameter or the chunk parameter,
+there is no conflict.
+
+>>If the data structure is only being read (a quite
+>>common occurrence), then there is no conflict.
+
+>Our limited experience with users wanting parallel speedup is to write to a
+>collection, not only read.
+
+As mentioned above, you can do both using a parallel iterator.
+
+>>Tucker also noted the special cases for writing arrays.
+
+>What is that special case?
+
+When indexing into an array that is global to a parallel loop, so long as the
+index is the loop parameter or the chunk parameter, there is no conflict (see
+9.10.1(20/5)).
+
+****************************************************************
+
+From: Richard Wai
+Sent: Wednesday, October 16, 2019 10:51 AM
+
+> I agree with Yannick. For me this is wishful design at best. "Planning" for
+> the future when you're not sure what the future is, in terms of language
+> design seems like a very bad idea, a good way to put a lot of features that
+> won't be used. If your planning was wrong, this "careful language design"
+> you're talking about will just be dead weight, while those other people
+> will still have to conceive the solution that is actually right for them.
+
+> For me, one such example in Ada is safety rules wrt. access types in
+> general: Those have proved to be overly restrictive, to the point of making
+> pool specific access types in Ada unusable for a variety of use cases. The
+> result have just been people circumventing the "safety".
+
+I strongly disagree with this. Ada often gets flack for these types of things
+as being "overly restrictive". However in my very practical experience, it has
+always been a sign of the programmer either not thinking through the problem
+correctly, or trying to force the style of other languages into Ada. If you
+follow software engineering principles carefully, show a little discipline,
+and really think through the problem properly, I have yet to find a case
+where pool-specific access types (or any access types) stand in the way. And
+again, if a programmer finds this to be a problem, they are probably
+approaching the problem poorly.
+
+If we don't plan for the future, then what are we going to get? The only other
+approach I could think of is to be broadly less restrictive, and fall-back
+into a "programmer knows best" approach. If we do that, we all might as well
+just use C++.
+
+I think the software industry at large really needs to spend some thing
+reflecting on the prevailing "just let me do whatever I want" attitude. You
+don't hear electrical engineers complaining about ringing, and how they can't
+make right-angle traces on PCBs. You don't hear mechanical engineers
+complaining about thermal expansion. You don't hear structural engineers
+complain about wind loads. And none of them have stopped innovating because of
+those things. The rules for access types in Ada are sane and reasonable. And
+if you accept them for what they are, and they are not C pointers, you will
+design your software around them, and you'll get rewarded with a very high
+degree of safety.
+
+Ada is about discipline. Ada is about strongly encouraging the programmer to
+do things with more care. It also allows managers to spot sloppy and unsafe
+code more easily. Ada is about exact rules. Ada is about planning ahead.
+
+Everyone plans for the future. It's simply lazy not to. Yes you can't always
+get it right, but the benefits of doing so are not predicated on getting it
+exactly right.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, October 16, 2019 3:10 PM
+
+> enough said, I was trying to have a technical discussion, not personal
+> attacks.
+
+But this is (now) more of a philosophical discussion than a technical
+discussion. You don't seem to think that safety in this area is achievable,
+and I not only think that it is, but also that Ada cannot continue with it.
+Unless we can agree on that point, there is nothing further to talk about,
+because all of the technical issues stem from that philosophy.
+
+In any case, I apologize if you took the above as a personal attack. I was
+just trying to restate my understanding of your position, and did it badly.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, January 14, 2020 11:41 AM
+
+In AI12-0079-2, there is mention of a document describing a simpler consensus
+proposal for Global developed by Claire and Tuck at AdaCore. Here is the
+content of that document. Note that in the "overview notes" at the end of the
+!discussion for AI12-0079-2, an attempt is made to record to what degree the AI
+goes beyond the consensus document. Most of these additions were alluded to
+below as "possible extensions" or as extensions to handle "indirect effects."
+Several AdaCore folks have indicated they are not in favor of any of the
+additions, or have not had enough time to evaluate them.
+
+-----------
+
+Simplified Global Aspect for Ada202X
+
+SYNTAX
+
+ 1 - Global aspects can be supplied on subprograms, tasks, and entries in
+ order to document the set of global objects they access, and how they
+ access them.
+
+ 2 - These contracts associate a mode, "in", "in out", or "out", to a set of
+ names. Modes in out and out would effectively be the same for the
+ compiler, but they could make a difference for other tools (SPARK,
+ CodePeer...). These names can be:
+ * Global constants
+ * Global variables
+ * A package entity Pack if the contract is located somewhere which does
+ not have visibility over the body of Pack. Here it stands for the
+ private state of Pack.
+ * "all" to state that the subprogram could read or write any global. It
+ may be used to forbid the usage of some subprograms.
+
+ 3 - Special values of the Global contract can be:
+ * "null" to state that no globals are accessed
+
+ * "Unspecified" to state that no globals have been supplied for this
+ entity. This would be the default. A restriction
+ No_Unspecified_Globals will be available for projects which choose to
+ require a more precise description of the global effects.
+
+ * "Synchronized", to state that there are references to an unspecified
+ set of synchronized objects. Because such objects are typically
+ volatile, there is no significant value in being more specific about
+ synchronized objects, as far as "in" vs. "in out". "Synchronized" can
+ be combined in a Global aspect specification with more precise
+ descriptions of the side effects on non-synchronized objects.
+
+CHECKS
+
+ 4 - If a subprogram mentions a global variable, this variable must be in the
+ global contract for the subprogram. If the variable is not visible at the
+ point of the subprogram declaration, the package private state is
+ considered to be mentioned instead.
+
+ 5 - If a subprogram writes to a global variable, this variable must be in the
+ global contract for the subprogram, and its mode should be either out or
+ in out. If the variable is not visible at the point of the subprogram
+ declaration, the package private state is considered to be written
+ instead.
+
+ 6 - When a subprogram calls another subprogram:
+
+ * Names mentioned in the global contract of the callee are considered to
+ be mentioned by the caller.
+
+ * Names mentioned in the global contract of the callee with modes out or
+ in out are considered to be written by the caller.
+
+ * If some package private state occurs in the global contract of the
+ called subprogram, and the specification of the caller does have
+ visibility on the body of the package, then the global contract of the
+ caller is expressed in terms of the package private state for the
+ check.
+
+ 7 - No checks are performed when checking a subprogram with Unspecified as a
+ global annotations, and no checks are associated with the global contract
+ of a callee if the callee has Unspecified as a global.
+
+ 8 - A subprogram with a synchronized global annotation, can mention any
+ variables which are synchronized, in addition to those stated explicitly
+ in its Global aspect.
+
+POSSIBLE EXTENSIONS
+
+ * Allowing a way to refer to the global contract of a formal parameter
+ of a generic unit in the global contract of generic subprograms or
+ subprograms in generic packages (eg. using Subp'Global).
+ * Having a way to change the default at the package level, at least to
+ put it to null or synchronized.
+
+ACKNOWLEDGEMENTS
+
+The Global aspect does not in general cover all the global effects of a
+subprogram. In particular, just like for parameter modes, effects on aliased
+data, or on data designated through a pointer would not necessarily occur in the
+Global contract of a subprogram.
+
+procedure Write_To_All (X : My_Access_Type) is
+begin
+ X.all := Some_Value; -- OK
+end Write_To_All;
+
+procedure Write_To_All with
+ Global => (in => X) is
+begin
+ X.all := Some_Value; -- OK
+end Write_To_All;
+
+Coming up with a good way to handle (some of) these cases would require time and
+prototyping, so would best be handled through an RFC.
+
+As a part of this work on a better handling of indirect effects, it may be
+necessary to tackle the problem of imprecise parameter modes as well.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, January 15, 2020 7:03 PM
+
+...
+>I believe that, to improve user experience, we should use the
+>under-approximation (ie do not take into account modification under an
+>access).
+
+I wanted to clarify my comments during the meeting on this topic, as I know that
+many of us have a better understanding of the issues when we read it and can
+digest it (as opposed to hearing it and having it quickly disappear, not to
+mention it is hard to understand complex positions from a 30-second summary over
+a fuzzy audio connection).
+
+My primary objection to Claire's document is summarized by this
+"under-approximation" sentence. The reason is that pretty much every use of
+Global that I can imagine requires an "over-approximation". (I'm assuming for
+this argument, like Claire, that an exact result is practically impossible, at
+least for the full unrestricted Ada language.)
+
+The intended use of Global as part of the checking to make parallel operations
+acceptably safe, for instance, requires that access dereferences be excluded
+unless provably safe. It's not helpful to detect only a few cases of obvious
+problems. Without strong checking, "parallel" is an attractive hazard that would
+make Ada substantially less safe.
+
+Similarly, I would like to use this information for optimization of many sorts.
+Currently, Janus/Ada assumes that every call "kills all", as there is no useful
+information to the contrary (Pure allows far too much to be useful in this way).
+Ada contains permissions that go too far and not far enough at once (the
+permissions don't take all of the parameters into account, and do prevent any
+optimization even when it is clear that only erroneous execution could change
+the results).
+
+Some of the optimizations in question include removing redundant checks (which
+of course can't be done if the checked value changes between the checks of
+interest), removing redundant calls (when the second call has no effect other
+than wasting time), and the like.
+
+Again, any undetected global access makes this sort of thing impossible.
+
+It seems to me that much the same situation occurs for verification. A
+side-effect potentially invalidates much of what is known before a call, and one
+that it hidden from a verifier is going to mean that invalid assumptions may
+hold. (Optimization and verification have much the same requirements.)
+
+I agree that the "user experience" is important, but if the aspect isn't
+providing the needed guarantees, then it doesn't matter very much as it won't be
+used very often.
+
+I note in passing that in my recent code, probably 20% of the subprograms could
+be Global => null, and probably another 40% could be Global => in all, even with
+the most conservative rule (that is, a dereference is only covered by "all").
+These are all opportunities for parallel usage and for optimization (which
+includes checking code elimination, redundant store elimination, and many more).
+
+I've been planning to build something like this with or without language
+support, but obviously I'd prefer to use something supported by the language (it
+reduces the chance of missing corner cases and the like). So I would hope that
+we can find a way to support Global that I (and presumably others) would find
+useful.
+
+One possible way to do so would be to have a configuration mode that determines
+whether under-specification or over-specification is required for Global.
+Presumably SPARK would use the under-specified mode, and Janus/Ada would treat
+anything compiled in the under-specified mode as "unknown" for any
+implementation-defined uses (optimizations, warnings, etc.) Such a mode would
+determine how dereferences are handled (either ignored or required to be covered
+with "all" of the correct mode), and probably ought to have some effect on how
+library-level "unspecified" is handled as well ("in out all" unless the
+implementation can prove better).
+
+****************************************************************
+
+From: Claire Dross
+Sent: Thursday, January 16, 2020 8:21 AM
+
+> I agree that the "user experience" is important, but if the aspect
+> isn't providing the needed guarantees, then it doesn't matter very
+> much as it won't be used very often.
+
+All depends on what you call needed guarantees I suppose. We are back to the
+initial question, what do we want this aspect to be used for. I think that the
+"complement of to the parameter list" is already interesting. But I understand
+that you disagree.
+
+> I note in passing that in my recent code, probably 20% of the
+> subprograms could be Global => null, and probably another 40% could be
+> Global => in all, even with the most conservative rule (that is, a
+> dereference is only covered by "all"). These are all opportunities for
+> parallel usage and for optimization (which includes checking code
+> elimination, redundant store elimination, and many more).
+
+Interesting. Do those 20% use pointers at all? If not, maybe a restriction
+asking for no pointer dereference could reconcile the two views?
+
+> I've been planning to build something like this with or without language
+> support, but obviously I'd prefer to use something supported by the language
+> (it reduces the chance of missing corner cases and the like). So I would
+> hope that we can find a way to support Global that I (and presumably others)
+> would find useful.
+>
+> One possible way to do so would be to have a configuration mode that
+> determines whether under-specification or over-specification is required for
+> Global. Presumably SPARK would use the under-specified mode, and Janus/Ada
+> would treat anything compiled in the under-specified mode as "unknown" for
+> any implementation-defined uses (optimizations, warnings, etc.) Such a mode
+> would determine how dereferences are handled (either ignored or required to
+> be covered with "all" of the correct mode), and probably ought to have some
+> effect on how library-level "unspecified" is handled as well ("in out all"
+> unless the implementation can prove better).
+
+My guess is that with the over-approximation, most (all?) subprograms
+using pointer dereferences would quickly get "in out all" (or at least
+"in all"). This is not bringing much information in my opinion... Also
+remark that, without any proper checking of aliasing, no optimization of
+anything which does not have Global null would really be safe (even in
+the absence of pointers). Thus I don't think the over-approximation case
+would be as valuable as you think: it would hardly ever bring valuable
+information on programs using pointers, and it would not provide
+complete safety. Maybe what you really want is something close to Pure
+which would mean global null?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, January 16, 2020 8:13 PM
+
+...
+> > I note in passing that in my recent code, probably 20% of the
+> > subprograms could be Global => null, and probably another 40% could
+> > be Global => in all, even with the most conservative rule (that is,
+> > a dereference is only covered by "all"). These are all opportunities
+> > for parallel usage and for optimization (which includes checking
+> > code elimination, redundant store elimination, and many more).
+>
+> Interesting. Do those 20% use pointers at all? If not, maybe a
+> restriction asking for no pointer dereference could reconcile the two
+> views?
+
+Probably not, most such routines take a record type and calculate something
+interesting with the components. But I am assuming that one can use the
+containers roughly as I annotated them last year (so there might be some
+pointers in the implementation).
+
+You're new here (and don't hang out on comp.lang.ada), so you probably haven't
+heard my oft-made opinion that a good ADT design for Ada uses no visible access
+types. (A very brief explanation: this lets the client control memory management
+explicitly with access types, by using Ada scoping, or by using a container. If
+you use access types, you end up taking on memory management yourself and that
+restricts how the client can use your abstraction.) I know many others disagree
+with this (and I tend to state in an abolutist way which makes a good soundbite
+but I realize that not every problem is the same), but I try to hold to that for
+most of my work. Thus, any pointers are hidden in the package and can be often
+be accounted for with some ownership scheme (or possibly even the simpler
+compound scheme that Tucker described in AI12-0240-6).
+
+Of course, all of these estimates are by eyeballing code, and once a
+compiler/tool starts checking it, the numbers and possibilities might change.
+:-) And I've got a lot of compiler code that predates when I knew anything about
+designing software!
+
+...
+> > One possible way to do so would be to have a configuration mode that
+> > determines whether under-specification or over-specification is required for
+> > Global. Presumably SPARK would use the under-specified mode, and Janus/Ada
+> > would treat anything compiled in the under-specified mode as "unknown" for
+> > any implementation-defined uses (optimizations, warnings, etc.) Such a mode
+> > would determine how dereferences are handled (either ignored or required to
+> > be covered with "all" of the correct mode), and probably ought to have some
+> > effect on how library-level "unspecified" is handled as well ("in
+> > out all" unless the implementation can prove better).
+>
+> My guess is that with the over-approximation, most (all?) subprograms
+> using pointer dereferences would quickly get "in out all" (or at least
+> "in all"). This is not bringing much information in my opinion...
+
+I expect that as well. In the case of uncontrolled access types (especially
+general access types), there really isn't much information to bring. You could
+use something like "aliased <type_name>" if the designated type is visible, but
+otherwise there is no possible way to describe what it points at.
+
+One probably can do better in with an ownership / compound object scheme, but
+that clearly requires restrictions on the access type. Given that Ada is likely
+to compete with languages like Rust that are working in this area, it's an area
+that we need to be looking at. (Whether we can do something standardizable for
+Ada 202x is of course worth discussing, but it's an area that we need to be
+working in, IMHO.)
+
+But for the sorts of uses I'm primarily thinking about, even "in all" brings a
+lot of benefits: A parallel loop can call such a routine safely; the information
+known before a call to an "in all" subprogram is still known afterwards (modulo
+parameter changes, which are explicitly in the code); and probably with the most
+benefit, a redundant call can be part of a common subexpression assuming there
+are no global writes between the calls. (And I want to use the last effect to
+help verify preconditions and postconditions.)
+
+> Also remark that, without any proper checking of aliasing, no optimization of
+> anything which does not have Global null would really be safe (even in
+> the absence of pointers).
+
+A compiler optimizer can't do anything if it can't rule out aliasing, so I don't
+quite see the problem. "Assume-the-worst" is pretty much always the watchword
+for optimization.
+
+There are cases that can't be detected (like chapter 13 stuff), but these are
+explicitly erroneous. And optimization explicitly assumes that the code isn't
+erroneous (without such an assumption, there is virtually nothing that could be
+done, since erroneous code can write any memory location at any time).
+
+Formally, if execution is erroneous (which means that anything can happen), then
+any transformation is acceptable (since the result will still be that anything
+can happen, even if it is different anything).
+
+> Thus I don't think the over-approximation case would be as valuable as
+> you think: it would hardly ever bring valuable information on programs
+> using pointers, and it would not provide complete safety. Maybe what
+> you really want is something close to Pure which would mean global
+> null?
+
+As noted above, "in all" is valuable by itself. Additional precision could be
+useful, but I don't think it is critical (as much of the time, one would still
+have a conflict as nearby operations tend to work on the same data structure,
+and if that structure has some global part, they all probably use it). It is
+necessary, I think, to have some way for "hidden" access types to be "erased"
+from the picture, since the containers need to be usable in tasks and parallel
+operations (and *definitely* need to be able to be optimized) -- and we want
+users to be able to build similar custom data structures if they need to.
+
+We did send this stuff back to Tucker, and I do trust Tucker to work his usual
+magic and find some way to cut this Gordian knot. The notion of splitting the
+Global stuff into an object part and an access part should help, as I don't
+think the object part is very controversial and that will allow us to make
+useful progress. (The new model for generics is definitely easier to work with
+than the one I came up with.) Part of my reason for discussing this here is to
+give him some parameters to work in.
+
+P.S. Back when we were working on Ada 2005 and Ada 2012, every time I passed
+through the Indianapolis area there were many billboards proclaiming "Trust
+Tucker!". I thought that was good advice. I rather regret that I was always on a
+busy freeway when I saw one of those and never got a picture for the ARG
+archives. They don't seem to be around anymore, hopefully that doesn't mean
+anything for the ARG. :-)
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Friday, January 17, 2020 2:17 AM
+
+> One probably can do better in with an ownership / compound object scheme,
+> but that clearly requires restrictions on the access type. Given that Ada is
+> likely to compete with languages like Rust that are working in this area,
+> it's an area that we need to be looking at. (Whether we can do something
+> standardizable for Ada 202x is of course worth discussing, but it's an area
+> that we need to be working in, IMHO.)
+
+Having worked for the past three years (with Tuck in particular) on defining
+rules for safe analysis of pointers, I think (1) this is an area of much
+interest for the future of Ada, and (2) it is not reasonable to expect something
+in a good enough shape by June. Or maybe you're proposing to delay Ada 202X to a
+later year, but that's not what we agreed on.
+
+If you're not convinced that it is complex, have a quick look at the excellent
+blog posts by Claire about the solution we adopted in SPARK:
+https://blog.adacore.com/using-pointers-in-spark
+https://blog.adacore.com/pointer-based-data-structures-in-spark
+(this is the easy introduction, not the nitty-gritty details)
+
+> A compiler optimizer can't do anything if it can't rule out aliasing, so I
+> don't quite see the problem. "Assume-the-worst" is pretty much always the
+> watchword for optimization.
+
+I don't see optimization being a major reason for investing in safe
+pointer/aliasing handling. It has not popped up elsewhere AFAIK, not in the Rust
+world either, unless you have more info here?
+
+> It is necessary, I think, to have some way for "hidden" access types to
+> be "erased" from the picture, since the containers need to be usable in
+> tasks and parallel operations (and *definitely* need to be able to be
+> optimized) -- and we want users to be able to build similar custom data
+> structures if they need to.
+
+Reasonably, the only choice we have is to trust their implementation for now.
+
+> We did send this stuff back to Tucker, and I do trust Tucker to work his
+> usual magic and find some way to cut this Gordian knot. The notion of
+> splitting the Global stuff into an object part and an access part should
+> help, as I don't think the object part is very controversial and that will
+> allow us to make useful progress.
+
+Being someone who spent a lot of time discussing it with Tuck and others over
+the past years, I don't understand how you expect a magic solution to pop up by
+June. By all accounts, it's too late IMO, whatever clever solution is proposed
+by Tuck or someone else, we won't have the time to properly assess it.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Friday, January 17, 2020 4:56 AM
+
+> I don't see optimization being a major reason for investing in safe
+> pointer/aliasing handling. It has not popped up elsewhere AFAIK, not
+> in the Rust world either, unless you have more info here?
+
+Well, pretty much all Java compilers do escape analysis, which involves a
+variant of aliasing analysis, and the resulting optimizations are plenty and
+important. Admittedly, afaik, they drop everything in the presence of subcalls
+that potentially create aliases of the local references, but I could be
+underestimating them. I don't know why Ada compilers haven't started similar
+analyses for reference types.
+
+As to the program analysis world:
+In almost all of our tools for embedded systems, aliasing analysis for stack
+pointers is really essential. Not a rough over-estimation, but a more refined
+analysis as accurate as we can afford to make it time-wise. Heap pointers, on
+the other hand are rather irrelevant today (way too difficult and hardly used
+in embedded code except for inroads of simple OOP, when the languae gives you
+no choice but to use references). Extrapolating a bit to the future: ...
+except when you can do the analogon of (a global) escape analysis
+successfully.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, January 17, 2020 7:26 AM
+
+...
+>> We did send this stuff back to Tucker, and I do trust Tucker to work his
+>> usual magic and find some way to cut this Gordian knot. The notion of
+>> splitting the Global stuff into an object part and an access part should
+>> help, as I don't think the object part is very controversial and that will
+>> allow us to make useful progress.
+
+> Being someone who spent a lot of time discussing it with Tuck and others
+> over the past years, I don't understand how you expect a magic solution to
+> pop up by June. By all accounts, it's too late IMO, whatever clever solution
+> is proposed by Tuck or someone else, we won't have the time to properly
+> assess it.
+
+Randy and I have discussed something very simple (and quite different from
+past approaches) which would address at least his concerns -- it was actually
+suggested by something that Claire said during the ARG meeting. So stay
+tuned ...
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, January 17, 2020 6:10 PM
+
+>Having worked for the past three years (with Tuck in particular) on defining
+>rules for safe analysis of pointers, I think (1) this is an area of much
+>interest for the future of Ada, and (2) it is not reasonable to expect
+>something in a good enough shape by June. ...
+
+As someone who has spent considerable time working with Tucker to refine and
+improve his proposals from an Ada perspective, I agree with you on the
+importance, and disagree with you on the possibility. I have a workable proposal
+for Ada that is fully checked and adds no erroneousness (it's also rather easy
+to implement in Janus/Ada, can't speak to other compilers). But that solution is
+unlikely to work for SPARK, and the checks potentially could be rather
+expensive.
+
+I'd hope that the SPARK people here could come up with something, but if they
+can't, we have to face the question of whether we want to leave *Ada* without a
+workable solution for another 5-ish years in order to let SPARK catch up. To me,
+that is likely to cede all of the mindshare to other languages like Rust. We
+need to have some new things to attract new people to Ada, because if we don't,
+the customer base will almost certainly gradually dwindle.
+
+>>A compiler optimizer can't do anything if it can't rule out aliasing,
+>>so I don't quite see the problem. "Assume-the-worst" is pretty much
+>>always the watchword for optimization.
+
+>I don't see optimization being a major reason for investing in safe
+>pointer/aliasing handling. It has not popped up elsewhere AFAIK, not in
+>the
+
+>Rust world either, unless you have more info here?
+
+Erhard answered this way better than I would have. I know from past discussions
+that AdaCore has not been very interested in the possibilities of Ada-aware
+optimization, while that probably has been my primary driver for the evolution
+of Janus/Ada. I don't want to sound like I'm asking for features specifically
+for Janus/Ada, but I don't want to see features in Ada that interfere with the
+sorts of uses I'm interested in (we need alternatives for no other reason that
+to push AdaCore; a single dominant implementation is certain to become stale
+eventually).
+
+>>It is necessary, I think, to have some way for "hidden" access types
+>>to be "erased" from the picture, since the containers need to be
+>>usable in tasks and parallel operations (and *definitely* need to be
+>>able to be
+>>optimized) -- and we want users to be able to build similar custom
+>>data structures if they need to.
+
+>Reasonably, the only choice we have is to trust their implementation
+>for now.
+
+There is two problems with the "trust" model: First, we have to define fairly
+carefully what the requirements actually are. If we don't do that, no one will
+even know what lines that they are allowed to color inside of. How can anyone
+trust my implementation if I don't even know what restrictions I'm supposed to
+follow? And second, if we have defined such lines, then I don't know how to
+determine if I (as the implementor of some ADT) actually have implemented
+something worthy of trust.
+
+To me, this requires some form of checking, because it is too hard to determine
+if the rules (whatever they are) are met. Ada almost never uses "trust" when
+verification is possible. And in the cases where it does use "trust" (for
+instance, interfaces), the consequences of breaking the trust are severe
+(erroneous execution). I think we all would rather have checks rather than new
+ways to make things erroneous.
+
+>>We did send this stuff back to Tucker, and I do trust Tucker to work
+>>his usual magic and find some way to cut this Gordian knot. The notion
+>>of splitting the Global stuff into an object part and an access part
+>>should help, as I don't think the object part is very controversial
+>>and that will allow us to make useful progress.
+
+>Being someone who spent a lot of time discussing it with Tuck and
+>others over the past years, I don't understand how you expect a magic solution to
+>pop up by June.
+
+Tucker sent me an outline of a solution yesterday which appeared to work (in
+part because it is based in part on AI12-0240-6, which I know would work). I
+already have a dynamic checking solution that works within those parameters
+(it's perhaps too expensive, but I'm hopeful that we can find some additional
+checks that could reduce the cost).
+
+>By all accounts, it's too late IMO, whatever clever solution is
+>proposed by Tuck or someone else, we won't have the time to properly assess it.
+
+We don't have to have every last detail worked out by June, only an scope
+determination. The ARG has almost a year to complete polishing the Standard
+after June. Clearly, we'll need a decent amount of detail to get buy in on the
+scope for this feature, but we can do work (such as wording) after June.
+
+In any case, I don't think my dynamic checking solution could work for SPARK. If
+that means that we simply publish it in an Annex or as a Technical Specification
+(that is, something that might be added to the Standard in the future), that
+would be OK with me. (AdaCore's customers and programmers could decide if they
+want it implemented.)
+
+I don't think that we can afford to wait to address these issues. In 5 years,
+other languages would have all of the mindshare in this area and there would be
+no way for Ada to get it back. (I think the same applies to parallel operations,
+even if we don't have an immediate need for them. Other languages already have
+these features and they'll be more widely understood in the future.)
+
+Ada 202x will need some things that will attract new users to Ada.
+Otherwise, Ada will just gradually lose users as they retire or move to other
+things. I don't think delta aggregates are going to excite anyone (although
+existing Ada users will find them handy).
+
+****************************************************************
+
+From: Richard Wai
+Sent: Friday, January 17, 2020 7:02 PM
+
+> I'd hope that the SPARK people here could come up with something, but
+> if they can't, we have to face the question of whether we want to
+> leave *Ada* without a workable solution for another 5-ish years in
+> order to let SPARK catch up. To me, that is likely to cede all of the
+> mindshare to other languages
+> like Rust. We need to have some new things to attract new people to
+> Ada, because if we don't, the customer base will almost certainly
+> gradually dwindle.
+
+I think this is a really important point. The ARG should be focused on Ada
+and only Ada. I don't think it is our concern how hard we make the lives of
+the SPARK team (sorry). It is great for us to discuss these issues and do what
+we can to accommodate SPARK where it makes sense, but It is simply wrong for
+SPARK to control Ada. It should be the other way around. It is equally
+inappropriate for AdaCore to dictate the ARG's work (as it is for any single
+party). If I recall correctly, the ARG has been working on this issue for quite
+some time, and AdaCore has been the primary resistance to most of the working
+proposals that we've had.
+
+I also not that there are plenty of execution contexts (basically 90% of those
+we work in) where exceptions are not only fine, they are important useful. These
+same contexts also make run-time checking similarly desirable and useful. SPARK
+is expensive, and simply not economic for a large number of situations where it
+provides no additional safety except preventing exceptions.
+
+> Erhard answered this way better than I would have. I know from past
+> discussions that AdaCore has not been very interested in the possibilities
+> of Ada-aware optimization, while that probably has been my primary driver
+> for the evolution of Janus/Ada. I don't want to sound like I'm asking for
+> features specifically for Janus/Ada, but I don't want to see features in
+> Ada that interfere with the sorts of uses I'm interested in (we need
+> alternatives for no other reason that to push AdaCore; a single dominant
+> implementation is certain to become stale eventually).
+
+To be totally fair, this has not played out for most languages in existence. The
+problem are proprietary implementations. And I don't mean this philosophically,
+I mean it factually: all of the popular languages in use today have
+unencumbered, free implementations. Full stop. Most of them have one or two
+implementations, tops. It's honestly a point of strength to have one reference
+implementation, but the software community, especially the younger of us, expect
+languages to be free. Period.
+
+Maybe some feature implementations we can help work on for FSF GNAT. It's
+something I'd be consider dedicating some time to.
+
+General-purpose languages that are tied to proprietary implementations are
+almost guaranteed to fail. It's not the 80s anymore.
+
+> Ada 202x will need some things that will attract new users to Ada.
+> Otherwise, Ada will just gradually lose users as they retire or move to
+> other things. I don't think delta aggregates are going to excite anyone
+> (although existing Ada users will find them handy).
+
+While I agree with this in principle, I strongly believe that Ada already has
+features that are far ahead of other comparable languages. Rust, the closest
+"competitor" to Ada, has a lot of problems - and I'd argue that this is mostly
+due to their single focus on memory safety and not much else. Let's not get
+caught up with who is the hottest kid on the block this year. In our practical
+experience, Ada already makes memory problems so rare that Rust doesn't really
+being anything superior to the table in terms of safety, reliability, or
+efficiency.
+
+More dangerous for Ada than not adding enough features is adding too many
+features for fickle reasons, especially for trying to win popularity contests or
+saying "me too".
+
+While I agree with you that we can't let SPARK hold back Ada, I'm not convinced
+that Ada is going to attract any new users on features. At best it will retain
+existing (probably commercial) users who are considering switching to other
+languages. If Ada wants to attract new users, it has to do it by being more
+accessible, and less commercial. If Ada wants to differentiate itself, it should
+do so by being the sane, mature, carefully designed language that is always has
+been. If it stops being that, it stops being special.
+
+Just my two cents (1.5 c USD)
+
+****************************************************************
+
+From: Claire Dross
+Sent: Friday, January 17, 2020 7:46 PM
+
+> Interesting. Do those 20% use pointers at all? If not, maybe a
+> restriction asking for no pointer dereference could reconcile the two
+> views?
+
+If we want to go this way, maybe we could consider requiring constants
+containing access-to-variable parts to be listed in the global contract (this
+could be fair, since in Ada, these constants really are variables).
+
+Then checking whether a subprogram is well-behaved (its global contract
++ parameters is an over-approximation of its effects) could be as simple
+as checking that its parameters / globals have no access-to-variable/aliased
+parts (please sanity check me on this, I am not that knowledgeable about the
+crazy things that can happen in full Ada).
+
+When we have ownership types, well-behaved subprograms could use them (provided
+we manage to make parameter mode consistent on them).
+
+****************************************************************
+
+From: Claire Dross
+Sent: Friday, January 17, 2020 8:57 PM
+
+Please, could we avoid adding fuel to the fire here? I think we are all working
+toward the same goal (making Ada a better language, and if possible more
+attractive) and I don't think a schism would serve anybody.
+
+As for SPARK, I think (I hope?) it may serve to bring people to Ada.
+This does not mean the ARG *should* take it into account when designing Ada. But
+it is just another tool of the eco-system, so I think that if something makes
+its life harder, it can be mentioned as a drawback, just like for any other tool
+for Ada.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, January 17, 2020 9:43 PM
+
+> > Interesting. Do those 20% use pointers at all? If not, maybe a
+> > restriction asking for no pointer dereference could
+> > reconcile the two views?
+>
+> If we want to go this way, maybe we could consider requiring constants
+> containing access-to-variable parts to be listed in the global
+> contract (this could be fair, since in Ada, these constants really are
+> variables).
+
+I believe the AI12-0079-1 proposal and its various fixes did that. Not sure if
+Tucker carried that over into the AI12-0079-2 proposal, but I would hope so. In
+full Ada, only a few "constants" are really known to be constant. See 3.3(13/3),
+specifically the part about "inherently mutable". This happens because of the
+possibility of writable self-pointers being constructed during initialization.
+
+The definition of "variable" that had to be included in Global was:
+
+ The Global aspect identifies the set of variables (which, for the purposes
+ of this clause includes all constants with some part being immutably
+ limited, or of a controlled type, private type, or private extension) global
+ to a callable entity ...
+
+(This is 6.1.2(12/5) in the Draft 23 RM:
+http://www.ada-auth.org/standards/2xaarm/html/AA-6-1-2.html.)
+
+Private types have to be included since Legality Rules depend on this
+definition, and we don't want to break privacy for high-level Legality Rules.
+(There are only a few rules that break privacy, and most are related to Chapter
+13 representation stuff.)
+
+This isn't as bad as it sounds, as there aren't that many library-level
+constants of private types (at least not in my code) -- those would require some
+sort of constructor which wouldn't be preelaborable. At least in my code, most
+of the constant globals are numbers and data tables which are none of the things
+above.
+
+> Then checking whether a subprogram is well-behaved (its global contract
+> + parameters is an over-approximation of its effects) could be as + simple
+> as checking that its parameters / globals have no
+> access-to-variable/aliased parts (please sanity check me on this, I am
+> not that knowledgeable about the crazy things that can happen in full Ada).
+
+See above. :-)
+
+> When we have ownership types, well-behaved subprograms could use them
+> (provided we manage to make parameter mode consistent on them).
+
+The "overriding" thing for the original Global proposal allowed changing the
+effective mode only for the purposes of Global. (You can see that in the wording
+for the draft 23 RM.) That or some equivalent functionality is kinda necessary
+if we're going to use this on packages like Text_IO and Discrete_Random (we
+hardly can change the modes at this late date in them). Users write stuff like
+that, too, probably because they're patterning on package like Text_IO and
+Discrete_Random. :-)
+
+****************************************************************
+
+From: Claire Dross
+Sent: Saturday, January 18, 2020 4:33 PM
+
+...
+> This isn't as bad as it sounds, as there aren't that many
+> library-level constants of private types (at least not in my code) --
+> those would require some sort of constructor which wouldn't be
+> preelaborable. At least in my code, most of the constant globals are
+> numbers and data tables which are none of the things above.
+
+I understand that, but I am not sure I think this is a good idea. I still feel
+like we are doing to much over-approximation for a compile time verification.
+When doing a static analysis tool, we are always faced to the difficult
+challenge of coming up with a correct trade-off between precision and
+correction. AFAIK, very few people are OK with having a tool emitting a lot of
+false alarms or require an heavy annotation burden, and so, even if the
+guarantees offered are important (full functional correctness, absence of
+RTE...). Unfortunately, this seems to be also true in safety critical domains
+(from the user feed-back we get on codepeer and spark). And I fear this feature
+will have too much of both (annotation burden +false alarms) for a limited
+interest. This is why I am trying to push toward something simple with as little
+annotation burden and as little false alarms as possible.
+
+...
+>> When we have ownership types, well-behaved subprograms could use them
+>> (provided we manage to make parameter mode consistent on them).
+> The "overriding" thing for the original Global proposal allowed
+> changing the effective mode only for the purposes of Global. (You can
+> see that in the wording for the draft 23 RM.) That or some equivalent
+> functionality is kinda necessary if we're going to use this on
+> packages like Text_IO and Discrete_Random (we hardly can change the modes
+> at this late date in them).
+> Users write stuff like that, too, probably because they're patterning
+> on package like Text_IO and Discrete_Random. :-)
+
+See above...
+
+****************************************************************
+
+From: Raphael Amiard
+Sent: Monday, January 20, 2020 4:56 AM
+
+>. Ada 202x will need some things that will attract new users to Ada.
+>> Otherwise, Ada will just gradually lose users as they retire or move to
+>> other things. I don't think delta aggregates are going to excite anyone
+>> (although existing Ada users will find them handy).
+
+> While I agree with this in principle, I strongly believe that Ada already
+> has features that are far ahead of other comparable languages. Rust, the
+> closest "competitor" to Ada, has a lot of problems - and I'd argue that this
+> is mostly due to their single focus on memory safety and not much else.
+> Let's not get caught up with who is the hottest kid on the block this year.
+> In our practical experience, Ada already makes memory problems so rare that
+> Rust doesn't really being anything superior to the table in terms of safety,
+> reliability, or efficiency.
+
+This attitude is really concerning to me. I'm seeing it play out everywhere in
+our community, and it is very strong at the ARG too. I did not yet have the
+pleasure to meet you in person at an ARG meeting but I have read a lot of your
+mails and I feel it too:
+
+"Our language is superior yet doomed, and other communities have not understood
+what makes it so great" (I'm making the strokes bold here).
+
+Rust has much more going for it than memory safety. Funnily enough, while we're
+trying to figure out how to do safe parallelism, they've actually had the
+problem solved since a few years ago
+(https://blog.rust-lang.org/2015/04/10/Fearless-Concurrency.html).
+
+Hint: ownership is not solely about memory. It's about resources, and aliasing
+of them, and having a sound static model to analyze those. This model is exactly
+what we're missing to make parallelism safe, hence very related to this AI.
+
+Beyond ownership, the trait system, a powerful generic model, and error handling
+that is much easier to statically analyse than Ada's unchecked exceptions are
+domains where you could claim that Rust is superior in terms of safety to Ada.
+
+There would be a debate, but outright claiming that Rust "only has memory
+safety" and Ada is "superior in every other way" is an over simplification of
+reality, to the point of being simply incorrect.
+
+> More dangerous for Ada than not adding enough features is adding too many
+> features for fickle reasons, especially for trying to win popularity
+> contests or saying "me too".
+
+I agree with you here. Actually I think there would be a lot more to do for
+Ada's popularity at the implementation/ecosystem/tooling/teaching level than at
+the language level.
+
+And even at the language level, reducing inconsistencies and making the language
+more globally coherent would be *much more valuable* than adding tons of new
+features:
+
+We're not C++. We don't have a large user base to try and keep, our user base is
+already pretty small, and they're not updating language versions (most of them
+at least). That means that if we're trying to attract users, they're going to be
+new users, or old users on new projects.
+
+> While I agree with you that we can't let SPARK hold back Ada, ...
+
+I'm going to be bold again, but in terms of popularity and appeal to programmers
+in the large, SPARK is one of the only reasons Ada is interesting to new users.
+In terms of safety it's a language that is in effect more safe than every other
+alternatives (including Rust), but yet more usable and production ready than
+other research-y alternatives. From my point of view it has the unique value
+proposition that Ada is missing (while still being a great language).
+
+****************************************************************
+
+From: Richard Wai
+Sent: Monday, January 20, 2020 11:14 AM
+
+> This attitude is really concerning to me. I'm seeing it play out everywhere
+> in our community, and it is very strong at the ARG too. I did not yet have
+> the pleasure to meet you in person at an ARG meeting but I have read a lot
+> of your mails and I feel it too:
+
+> "Our language is superior yet doomed, and other communities have not
+> understood what makes it so great" (I'm making the strokes bold here).
+
+I have never felt Ada was doomed, nor do I think it is broadly superior to
+everything. What I do think is that Ada is both unique and uniquely proven for
+general purpose programming - which is most programming. Rust is talking about
+things - safety and correctness - that Ada has been dealing with since 1983.
+Unlike Ada, Rust ignores all of the subtle but key ideas of readability, rich
+abstraction, separate compilation, and data modeling. Ada is not doomed, just as
+Rust is not proven. Let's please try to see the forest for the trees.
+
+> Beyond ownership, the trait system, a powerful generic model, and error
+> handling that is much easier to statically analyse than Ada's unchecked
+> exceptions are domains where you could claim that Rust is superior in
+> terms of safety to Ada.
+
+You mean the error handling model where you need to explicitly deal with every
+possibly return condition on every function, and if you don't deal with every
+possibility the entire program crashes? Yeah that sounds great for static
+analysis, but what about the programmer? That's brutal, and frankly the single
+worst part about programming in Rust, IMO. It's almost as bad as the try-catch
+approach to exception handling. Good thing we have Ada which handles these
+problems rationally, and in a way that is very natural and powerful to work
+with.
+
+> There would be a debate, but outright claiming that Rust "only has memory
+> safety" and Ada is "superior in every other way" is an over simplification
+> of reality, to the point of being simply incorrect.
+
+I'm not coming from a theoretical standpoint here, I'm coming from a purely
+practical standpoint. And this is an issue that I see as getting dangerously
+worse lately. I care about using Ada to build real applications - not to
+research computer science, or to reimplement someone's pet algorithm. Your (and
+others at AdaCore) fixation on static analysis concerns me. I understand the
+value of formal methods and static analysis, but I'm not sure your camp
+appreciates the practical viability (read: economics) in large, non
+safety-critical, non-embedded domains.
+
+For this point, suffice it to say that Rust has a lot of problems stemming from
+their very "nice on paper" approach, which has been less than nice in practice.
+Ownership is a neat concept, but used "in real life", it ends up being very
+restrictive and challenging to get actual work done. I mean actual work as in
+actual living applications or libraries that do real useful things, not cute
+little micro-package crates. I'm talking about large applications or frameworks
+that serve general needs. Rust is struggling with this issue now and the
+community knows it. Getting practical things to work in that ownership model
+leads to prevent and egregious use of "unsafe", defeating the entire purpose -
+take note of the recent Actix-web drama.
+
+Ada has tried very hard for very long to avoid falling into that trap - of
+making the user tempted to always turn off checking and use unsafe approaches,
+just to get the work done, because it's simply too difficult and time-consuming
+to do it otherwise. All this talk about Rust and ownership and safety always
+leaves out Ada's greatest strengths - strengths of structure, discipline, and
+realistic, rather than idealized rules. Ada is mature and realistic, Rust is
+not. And yes, it may be one day, but we are not going to compete with that by
+being less confident in Ada. What I'm saying is - let's not forget about the
+true strengths of Ada. You need to compare the strengths with the weakness, not
+in exclusion.
+
+> I'm going to be bold again, but in terms of popularity and appeal to
+> programmers in the large, SPARK is one of the only reasons Ada is
+> interesting to new users. In terms of safety it's a language that is in
+> effect more safe than every other alternatives (including Rust), but yet
+> more usable and production ready than other research-y alternatives. From
+> my point of view it has the unique value proposition that Ada is missing
+> (while still being a great language).
+
+Respectfully, is it the perspective of AdaCore? Otherwise I don't see how you
+can talking about what interests new users. Because new AdaCore users /= new Ada
+users. I should know, we are one of those new users. Unless you're a large
+corporation - say if you're startup, you're frankly going to be using FSF GNAT,
+not GNAT Pro. I've seen it time and again. The other userbase AdaCore likely
+sees is the academic community - which are unsurprisingly interested in
+theoretical things, so are unsurprisingly excited about SPARK. That's not to say
+that SPARK is not practical, it is. It's to say that SPARK is especially
+exciting to the theoretical-minded people.
+
+I think suggesting that SPARK is the only thing attracting new users to Ada is
+frankly hubris.
+
+Mainstream uses (like us) crucial to the future of Ada, if not the literal
+future of Ada. Users that develop mainstream software for mainstream problems -
+things like web applications, or enterprise business logic. This kind of
+software is becoming ever more critical, and benefits every more from
+reliability, safety, and security. But this is software that is very large and
+very dynamic, and is built by large teams on aggressive schedules. I say this
+future because if you want Ada to actually grow its user base - that's where the
+growth needs to happen, since that is where the vast majority of the action is.
+
+In these contexts, SPARK is limited to the specific parts where you need
+especially high performance or especially high safety and security. It is not
+economical to apply SPARK to very large applications where exceptions are not a
+concern - but that is somewhere where Ada shines. I argue vehemently that Ada is
+better at building very large applications than any other language in practical
+use today. And this is where most problems with software lies - problems that
+arise from complexity, maintenance, and testing. Problems in keeping separate
+teams out of eachother's hair. These are all immensely valuable traits. And they
+are not things that SPARK or Rust do anything about. Static analysis and formal
+methods do not make software easier to read - but that's actually where software
+spends most of its time.
+
+Look, we love SPARK, it's very cool - but it is not practical as the main
+language of use for general-purpose software. Ada is. I'm increasingly concerned
+that the SPARK people, and AdaCore at large, want to make Ada less
+general-purpose, and more niche than it already is. I think that is a travesty
+because Ada was always designed to be general-purpose, and was always designed
+for "programming in the large". And you should know that I will fight
+tooth-and-nail to make this point heard.
+
+****************************************************************
+
+From: Raphael Amiard
+Sent: Friday, January 31, 2020 7:45 AM
+
+I took a very long time to answer that, because a lot of what you write seems
+exactly like the kind of unsubstantiated claims that I was trying to avoid in
+the first place.
+
+In some places what you write is subjective opinions stated as truth, like "Ada
+is mature and realistic, Rust is not".
+
+In other places, it's simply completely inaccurate, like your vision of the use
+of Rust today, in "micro"/"cute"/"toy" frameworks, disregarding the heaps of
+very serious production software that is being written with Rust today. You're
+perfectly capable of finding this information, should you wish to do so, but
+just to cite a few examples:
+
+- Mozilla Firefox ships with a large portion of code written in Rust nowadays
+- A large part of Cloudflare's infrastructure is written in Rust
+- Amazon has an hypervisor used in production written in Rust
+
+This extends to your opinions on language design and features, such as error
+handling. I'll send you an article that I truly love about error handling,
+http://joeduffyblog.com/2016/02/07/the-error-model/, that I'd highly advise
+anyone to read. It is highly articulate, documented, argumented, and balanced,
+making it clear that if there was a silver bullet we would probably have found
+it some time ago.
+
+Your position as you expressed it in the previous message, lacks those
+qualities. It's black and white and full of contempt. For me, while this is a
+common way of writing on, for example, comp.lang.ada (which is regrettable in
+itself) this is definitely not acceptable in a forum where professionals conduct
+language design. We should at the very least be able to have reasonable and
+documented positions, and, most importantly, balanced positions, where we
+acknowledge the complexity of our field and of the drawbacks game that language
+design is.
+
+Please think over this and the tone of your message, in particular with regards
+to Rust (I'll brush over the SPARK/AdaCore part since it's a very different
+topic, and you already discussed it a bit with Arnaud). Also please consider
+that it should be part of your duty as an ARG member to have balanced positions
+on such topics, and know the pros and cons of various approaches. It might be
+the case, but if it is, you didn't show it in your message.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, January 31, 2020 4:27 PM
+
+> I took a very long time to answer that, because a lot of what you write
+> seems exactly like the kind of unsubstantiated claims that I was trying to
+> avoid in the first place.
+
+Not sure who or what you are responding to since you didn't quote any of it.
+
+...
+>We should at the very least be able to have reasonable and documented
+>positions, and, most importantly, balanced positions, where we acknowledge
+>the complexity of our field and of the drawbacks game that language design
+>is.
+
+That's not the reality of e-mail discussions. Most of us here were "trained"
+by Robert Dewar to respond quickly to relevant messages, and that necessarily
+is going to cause positions that aren't as thought out as would be ideal.
+Moreover, most of us can't spend 4 hours pondering positions and alternatives
+and researching every topic that comes up, especially given the volume of mail
+on this list. I've made many points over the years that distracted from the
+critical topic and that I find embarassing when I reread them while filing
+mail. (And just as many questions I wish I had asked at the time.) That's the
+nature of the beast.
****************************************************************
Questions? Ask the ACAA Technical Agent