CVS difference for ai12s/ai12-0240-1.txt

Differences between 1.2 and version 1.3
Log of other versions for file ai12s/ai12-0240-1.txt

--- ai12s/ai12-0240-1.txt	2017/10/12 03:45:21	1.2
+++ ai12s/ai12-0240-1.txt	2017/11/30 04:18:02	1.3
@@ -558,7 +558,7 @@
 any actual compiler did for such things, meaning that every vendor would have
 to bifurcate their flow work (much as every vendor has to split compile-time
 expression evaluation into static and non-static parts). That's going to be a
-lot of work even for compiler's that already do the needed analysis.
+lot of work even for compilers that already do the needed analysis.
 
 It also seems that this sort of requirement would also require abandoning all
 pretense of a contract model for generics. (You all know where I stand on
@@ -609,7 +609,7 @@
 > references is so painful.
 
 You didn't give that as a rationale! The only thing the AI talks about is
-roving programs and eliminating aliasing.
+proving programs and eliminating aliasing.
 
 I'm surely not against "safe storage management" (that would be like being
 against apple pie!), but I don't see how the features in the AI provide
@@ -677,3 +677,48 @@
     types).
 
 ****************************************************************
+
+From: Raphael Amiard
+Sent: Thursday, October 12, 2017  9:11 AM
+
+> I noted that the !problem seems to concentrate totally on the problems 
+> of static analysis tools. It starts:
+>
+> "When attempting to prove properties about a program, ..."
+>
+> I'd argue that a large proportion of Ada users aren't planning to do 
+> that anytime soon. And arguably, static analysis tools can solve their 
+> own problems (as you say is being done with SPARK). So what's the 
+> value of this proposal to the average Ada user?
+
+In my opinion you're drawing a line in the sand that is not so clearly
+delimited. A static type system like the one Ada has exists to prove
+properties about a program, and it is part of the compiler, not of an external
+static analysis tool.
+
+In this instance, the value of this proposal is to solve a class of memory 
+problems in the language directly, instead of relying on static analysis
+tools to do it, IMHO.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, October 12, 2017  10:35 PM
+
+My point, which I may not have made so well, is that the Problem statement/
+Proposal explanation ought to spend at least some time on the benefits to
+people who aren't using formal static analysis tools. To only talk about proof
+issues leaves a lot of us out. 
+
+My understanding was that such techniques could be used to make programs that
+don't use any tools safe (which Tucker also said in his reply to me). The AI
+needs to emphasize that to get more broad-based support.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, October 13, 2017  6:36 AM
+
+Agreed.  The rationale was inadequate.
+
+***************************************************************

Questions? Ask the ACAA Technical Agent