comp.lang.ada
 help / color / mirror / Atom feed
* Intervention needed?
@ 2019-03-08 16:43 Olivier Henley
  2019-03-08 16:58 ` Dmitry A. Kazakov
                   ` (5 more replies)
  0 siblings, 6 replies; 146+ messages in thread
From: Olivier Henley @ 2019-03-08 16:43 UTC (permalink / raw)


Maybe someone with all the proper ammunitions could enlighten this user:

https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/11

Thx

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-08 16:43 Olivier Henley
@ 2019-03-08 16:58 ` Dmitry A. Kazakov
  2019-03-08 17:31 ` gautier_niouzes
                   ` (4 subsequent siblings)
  5 siblings, 0 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-08 16:58 UTC (permalink / raw)


On 2019-03-08 17:43, Olivier Henley wrote:
> Maybe someone with all the proper ammunitions could enlighten this user:
> 
> https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/11

That user wants pointers, he is beyond salvation.

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


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-08 16:43 Olivier Henley
  2019-03-08 16:58 ` Dmitry A. Kazakov
@ 2019-03-08 17:31 ` gautier_niouzes
  2019-03-11 14:31   ` antispam
  2019-03-11 15:34 ` Lucretia
                   ` (3 subsequent siblings)
  5 siblings, 1 reply; 146+ messages in thread
From: gautier_niouzes @ 2019-03-08 17:31 UTC (permalink / raw)


You could mention that you can can have dynamically sized variables or objects on the stack, thanks to unconstrained types. No pointers at all, no heap allocation.

For complex cases like trees, linked lists, etc. you can use the Ada.Containers which have deterministic (then predictable) garbage collection via finalization.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-08 17:31 ` gautier_niouzes
@ 2019-03-11 14:31   ` antispam
  2019-03-11 15:07     ` gautier_niouzes
  2019-03-11 17:19     ` Dmitry A. Kazakov
  0 siblings, 2 replies; 146+ messages in thread
From: antispam @ 2019-03-11 14:31 UTC (permalink / raw)


gautier_niouzes@hotmail.com wrote:
> You could mention that you can can have dynamically sized variables or objects on the stack, thanks to unconstrained types. No pointers at all, no heap allocation.
> 
> For complex cases like trees, linked lists, etc. you can use the Ada.Containers which have deterministic (then predictable) garbage collection via finalization.

Major issue with dynamically sized variables is running out of
memory.  How do you solve this?  Note that in modern environment
stacks tend to be tiny compared to heap, so this problem is
much more serious when using stack allocation.

-- 
                              Waldek Hebisch


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 14:31   ` antispam
@ 2019-03-11 15:07     ` gautier_niouzes
  2019-03-11 17:19     ` Dmitry A. Kazakov
  1 sibling, 0 replies; 146+ messages in thread
From: gautier_niouzes @ 2019-03-11 15:07 UTC (permalink / raw)


> Major issue with dynamically sized variables is running out of
> memory.  How do you solve this?

Unless you have infinite memory, the only solution it to have control of the maximum of memory your program will consume.

> Note that in modern environment
> stacks tend to be tiny compared to heap, so this problem is
> much more serious when using stack allocation.

That's for the default stack size; normally it is possible to adjust that, with limitations depending on the system. There are also separate settings (for GNAT, and perhaps other Ada systems) for size of the primary and secondary stacks.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-08 16:43 Olivier Henley
  2019-03-08 16:58 ` Dmitry A. Kazakov
  2019-03-08 17:31 ` gautier_niouzes
@ 2019-03-11 15:34 ` Lucretia
  2019-03-11 17:30   ` Simon Wright
                     ` (2 more replies)
  2019-03-13 13:23 ` Olivier Henley
                   ` (2 subsequent siblings)
  5 siblings, 3 replies; 146+ messages in thread
From: Lucretia @ 2019-03-11 15:34 UTC (permalink / raw)


On Friday, 8 March 2019 16:43:50 UTC, Olivier Henley  wrote:
> Maybe someone with all the proper ammunitions could enlighten this user:
> 
> https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/11

Just tore them a new one :)

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 14:31   ` antispam
  2019-03-11 15:07     ` gautier_niouzes
@ 2019-03-11 17:19     ` Dmitry A. Kazakov
  1 sibling, 0 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-11 17:19 UTC (permalink / raw)


On 2019-03-11 15:31, antispam@math.uni.wroc.pl wrote:

> Major issue with dynamically sized variables is running out of
> memory.  How do you solve this?

It is a design problem. If you have a large variable allocated in a 
single chunk of memory that requires frequent resizing, you did 
something wrong or used a wrong implementation of the variable's type. 
Usually the former.

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 15:34 ` Lucretia
@ 2019-03-11 17:30   ` Simon Wright
  2019-03-11 17:42     ` Dmitry A. Kazakov
  2019-03-11 19:52   ` Olivier Henley
  2019-03-11 22:08   ` Jeffrey R. Carter
  2 siblings, 1 reply; 146+ messages in thread
From: Simon Wright @ 2019-03-11 17:30 UTC (permalink / raw)


Lucretia <laguest9000@googlemail.com> writes:

> On Friday, 8 March 2019 16:43:50 UTC, Olivier Henley  wrote:
>> Maybe someone with all the proper ammunitions could enlighten this user:
>> 
>> https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/11
>
> Just tore them a new one :)

I thought you were reasonably polite!

On access types .. not that you were writing a textbook, but

> type A is access T; – Can point to local types.

Points to objects on (a) heap

> type B is access all T; – Can point to types on the heap and locally.

Points to objects on (a) heap or on the stack or static

> type C is access not null T; – Exclude nulls.

not null access!

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 17:30   ` Simon Wright
@ 2019-03-11 17:42     ` Dmitry A. Kazakov
  2019-03-11 18:14       ` AdaMagica
  0 siblings, 1 reply; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-11 17:42 UTC (permalink / raw)


On 2019-03-11 18:30, Simon Wright wrote:
> Lucretia <laguest9000@googlemail.com> writes:

>> type A is access T; – Can point to local types.
> 
> Points to objects on (a) heap

On the default heap, unless another Storage_Pool is explicitly specified 
for A.

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


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 17:42     ` Dmitry A. Kazakov
@ 2019-03-11 18:14       ` AdaMagica
  0 siblings, 0 replies; 146+ messages in thread
From: AdaMagica @ 2019-03-11 18:14 UTC (permalink / raw)


Am Montag, 11. März 2019 18:42:57 UTC+1 schrieb Dmitry A. Kazakov:
> On 2019-03-11 18:30, Simon Wright wrote:
> > Lucretia writes:
> 
> >> type A is access T; – Can point to local types.
> > 
> > Points to objects on (a) heap
> 
> On the default heap, unless another Storage_Pool is explicitly specified 
> for A.

On *a* default heap (there may be several).

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 15:34 ` Lucretia
  2019-03-11 17:30   ` Simon Wright
@ 2019-03-11 19:52   ` Olivier Henley
  2019-03-11 20:04     ` Lucretia
  2019-03-11 22:08   ` Jeffrey R. Carter
  2 siblings, 1 reply; 146+ messages in thread
From: Olivier Henley @ 2019-03-11 19:52 UTC (permalink / raw)


On Monday, March 11, 2019 at 11:34:17 AM UTC-4, Lucretia wrote:
> On Friday, 8 March 2019 16:43:50 UTC, Olivier Henley  wrote:
> > Maybe someone with all the proper ammunitions could enlighten this user:
> > 
> > https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/11
> 
> Just tore them a new one :)

Nice shot Lucretia! Thx

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 19:52   ` Olivier Henley
@ 2019-03-11 20:04     ` Lucretia
  0 siblings, 0 replies; 146+ messages in thread
From: Lucretia @ 2019-03-11 20:04 UTC (permalink / raw)


On Monday, 11 March 2019 19:52:50 UTC, Olivier Henley  wrote:

> > Just tore them a new one :)
> 
> Nice shot Lucretia! Thx

:)

I think you lot should take on what's coming next. The "yeah but, yeah but, borrow checker does that, yeah but...blah...*face punch*" :D


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 15:34 ` Lucretia
  2019-03-11 17:30   ` Simon Wright
  2019-03-11 19:52   ` Olivier Henley
@ 2019-03-11 22:08   ` Jeffrey R. Carter
  2019-03-12  2:04     ` Lucretia
                       ` (2 more replies)
  2 siblings, 3 replies; 146+ messages in thread
From: Jeffrey R. Carter @ 2019-03-11 22:08 UTC (permalink / raw)



On 3/11/19 4:34 PM, Lucretia wrote:
 > On Friday, 8 March 2019 16:43:50 UTC, Olivier Henley  wrote:
 >> Maybe someone with all the proper ammunitions could enlighten this user:
 >>
 >> https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/11
 >
 > Just tore them a new one :)

As far as I can see, Rust's only innovation is safer pointers, but it still has 
a bad design that requires the use of pointers. In Ada, pointers are never 
needed.* So Ada is still safer when dealing with pointers, since you never need to.

Other than that, Rust seems to be a typical C-family language with all the 
dangers that implies. So Ada is significantly safer there, too.

*1st-order approximation. Probably 2nd and 3rd, too

-- 
Jeff Carter
"It's symbolic of his struggle against reality."
Monty Python's Life of Brian
78


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 22:08   ` Jeffrey R. Carter
@ 2019-03-12  2:04     ` Lucretia
  2019-03-12 13:17       ` Olivier Henley
  2019-03-12 16:32       ` Jeffrey R. Carter
  2019-03-13  9:10     ` Maciej Sobczak
  2019-03-29 17:38     ` Florian Weimer
  2 siblings, 2 replies; 146+ messages in thread
From: Lucretia @ 2019-03-12  2:04 UTC (permalink / raw)


On Monday, 11 March 2019 22:08:38 UTC, Jeffrey R. Carter  wrote:
> On 3/11/19 4:34 PM, Lucretia wrote:
>  > On Friday, 8 March 2019 16:43:50 UTC, Olivier Henley  wrote:
>  >> Maybe someone with all the proper ammunitions could enlighten this user:
>  >>
>  >> https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/11
>  >
>  > Just tore them a new one :)
> 
> As far as I can see, Rust's only innovation is safer pointers, but it still has 
> a bad design that requires the use of pointers. In Ada, pointers are never 
> needed.* So Ada is still safer when dealing with pointers, since you never need to.
> 
> Other than that, Rust seems to be a typical C-family language with all the 
> dangers that implies. So Ada is significantly safer there, too.
> 
> *1st-order approximation. Probably 2nd and 3rd, too

Go on that thread and explain that to them.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12  2:04     ` Lucretia
@ 2019-03-12 13:17       ` Olivier Henley
  2019-03-12 16:32       ` Jeffrey R. Carter
  1 sibling, 0 replies; 146+ messages in thread
From: Olivier Henley @ 2019-03-12 13:17 UTC (permalink / raw)


...
> > *1st-order approximation. Probably 2nd and 3rd, too
> 
> Go on that thread and explain that to them.

I laughed so much it woke up my girlfriend ... :)

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12  2:04     ` Lucretia
  2019-03-12 13:17       ` Olivier Henley
@ 2019-03-12 16:32       ` Jeffrey R. Carter
  2019-03-12 16:56         ` Lucretia
                           ` (2 more replies)
  1 sibling, 3 replies; 146+ messages in thread
From: Jeffrey R. Carter @ 2019-03-12 16:32 UTC (permalink / raw)


On 3/12/19 3:04 AM, Lucretia wrote:
> 
> Go on that thread and explain that to them.

I have no desire to register to post on a forum full of people who like to use 
pointers. It's bad enough being on one full of people who like to use anonymous 
access types.

-- 
Jeff Carter
"Pray that there's intelligent life somewhere up in
space, 'cause there's bugger all down here on earth."
Monty Python's Meaning of Life
61


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12 16:32       ` Jeffrey R. Carter
@ 2019-03-12 16:56         ` Lucretia
  2019-03-12 17:20           ` Lucretia
  2019-03-12 18:14         ` Olivier Henley
  2019-03-12 21:41         ` Randy Brukardt
  2 siblings, 1 reply; 146+ messages in thread
From: Lucretia @ 2019-03-12 16:56 UTC (permalink / raw)


On Tuesday, 12 March 2019 16:32:34 UTC, Jeffrey R. Carter  wrote:
> On 3/12/19 3:04 AM, Lucretia wrote:
> > 
> > Go on that thread and explain that to them.
> 
> I have no desire to register to post on a forum full of people who like to use 
> pointers. It's bad enough being on one full of people who like to use anonymous 
> access types.

Well, there's no point explaining it here.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12 16:56         ` Lucretia
@ 2019-03-12 17:20           ` Lucretia
  0 siblings, 0 replies; 146+ messages in thread
From: Lucretia @ 2019-03-12 17:20 UTC (permalink / raw)


On Tuesday, 12 March 2019 16:56:03 UTC, Lucretia  wrote:
> > I have no desire to register to post on a forum full of people who like to 

And people wonder why Ada isn't getting any traction when people who use the language won't support or promote it or it's qualities.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12 16:32       ` Jeffrey R. Carter
  2019-03-12 16:56         ` Lucretia
@ 2019-03-12 18:14         ` Olivier Henley
  2019-03-12 19:21           ` Lucretia
  2019-03-12 21:41         ` Randy Brukardt
  2 siblings, 1 reply; 146+ messages in thread
From: Olivier Henley @ 2019-03-12 18:14 UTC (permalink / raw)


On Tuesday, March 12, 2019 at 12:32:34 PM UTC-4, Jeffrey R. Carter wrote:
> I have no desire to register to post on a forum full of people who like to use 
> pointers. It's bad enough being on one full of people who like to use anonymous 
> access types.

Do you think Lucretia and I had the 'desire to register' to that forum?

It has nothing to do with ourselves... me my, my.

I suppose we did so to set the record straight about Ada to a community that has 'A LOT' of traction and think they are reinventing the wheel... by staying blind to Ada. 


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12 18:14         ` Olivier Henley
@ 2019-03-12 19:21           ` Lucretia
  2019-03-12 21:53             ` Randy Brukardt
  0 siblings, 1 reply; 146+ messages in thread
From: Lucretia @ 2019-03-12 19:21 UTC (permalink / raw)


On Tuesday, 12 March 2019 18:14:04 UTC, Olivier Henley  wrote:
> On Tuesday, March 12, 2019 at 12:32:34 PM UTC-4, Jeffrey R. Carter wrote:
> > I have no desire to register to post on a forum full of people who like to use 
> > pointers. It's bad enough being on one full of people who like to use anonymous 
> > access types.
> 
> Do you think Lucretia and I had the 'desire to register' to that forum?

Exactly.
 
> It has nothing to do with ourselves... me my, my.
> 
> I suppose we did so to set the record straight about Ada to a community that has 'A LOT' of traction and think they are reinventing the wheel... by staying blind to Ada.

It's also to do with the fact that Rust isn't all that either. It literally only adds the pointer ownership thing, nothing else, yet this is the hype this train is carrying and lods of people are getting on it, instead of getting on Ada.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12 16:32       ` Jeffrey R. Carter
  2019-03-12 16:56         ` Lucretia
  2019-03-12 18:14         ` Olivier Henley
@ 2019-03-12 21:41         ` Randy Brukardt
  2 siblings, 0 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-03-12 21:41 UTC (permalink / raw)


"Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> wrote in message 
news:q68mv0$rea$1@dont-email.me...
> On 3/12/19 3:04 AM, Lucretia wrote:
>>
>> Go on that thread and explain that to them.
>
> I have no desire to register to post on a forum full of people who like to 
> use pointers. It's bad enough being on one full of people who like to use 
> anonymous access types.

This made me laugh out loud. Thanks for brightening my day, Jeff!

                        Randy.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12 19:21           ` Lucretia
@ 2019-03-12 21:53             ` Randy Brukardt
  2019-03-13 10:50               ` Jere
                                 ` (2 more replies)
  0 siblings, 3 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-03-12 21:53 UTC (permalink / raw)


"Lucretia" <laguest9000@googlemail.com> wrote in message 
news:bba8f6a8-36ce-4bed-bd84-8a9ea7dc02f7@googlegroups.com...
> On Tuesday, 12 March 2019 18:14:04 UTC, Olivier Henley  wrote:
>> On Tuesday, March 12, 2019 at 12:32:34 PM UTC-4, Jeffrey R. Carter wrote:
...
>> It has nothing to do with ourselves... me my, my.
>>
>> I suppose we did so to set the record straight about Ada to a community
>> that has 'A LOT' of traction and think they are reinventing the wheel... 
>> by staying blind to Ada.
>
> It's also to do with the fact that Rust isn't all that either. It 
> literally only adds the
> pointer ownership thing, nothing else, yet this is the hype this train is 
> carrying and
>  lods of people are getting on it, instead of getting on Ada.

My understanding is that the SPARK people are far into designing ownership 
contracts for Spark.

It's also possible that Ada 2020 will have a form of pointer ownership. 
(Unfortunately, we didn't make any conclusions on that during yesterday's 
meeting, so it's still in limbo, and we're getting very close to the finish 
line.) The current problem is that in Ada 2020 as it stands, it's not 
possible to write a containers implementation in pure Ada. You'd have to 
have some implementation hack to turn off some of the Legality Rules. Tucker 
has designed a solution, based on an ownership mechanism, but as it is new 
and barely vetted, it's unclear what we will do with it ultimately. Note 
that this solution will not provide the perfect safety that you would get 
with SPARK or Rust, but it would form the foundation of the SPARK solution 
and it would clearly catch a lot of issues with using pointers to implement 
ADTs. (And there is little other reason to use pointers, IMHO.)

                            Randy.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 22:08   ` Jeffrey R. Carter
  2019-03-12  2:04     ` Lucretia
@ 2019-03-13  9:10     ` Maciej Sobczak
  2019-03-13 11:08       ` Jere
  2019-03-13 13:44       ` Olivier Henley
  2019-03-29 17:38     ` Florian Weimer
  2 siblings, 2 replies; 146+ messages in thread
From: Maciej Sobczak @ 2019-03-13  9:10 UTC (permalink / raw)


OK, playing the devils's advocate again.

> As far as I can see, Rust's only innovation is safer pointers,

Which is, arguably, the innovation many people have been waiting for.

> but it still has 
> a bad design that requires the use of pointers.

Why it is bad?
Before, the criticism of pointers was based on the fact that pointers are dangerous. So, Ada is better, because it avoids these dangers.
Now we have guys with *safe* pointers and what? They are bad, because they use pointers? And pointers are bad, because they are dange... wait, something's went wrong.

If the problem with pointers is that they are dangerous, then safe pointers solve that problem. No?

> In Ada, pointers are never 
> needed.

And, surprise, nobody cares. Because now their pointers are safe.

> Other than that, Rust seems to be a typical C-family language with all the 
> dangers that implies.

What dangers? Like for example pointers? Oh, wait...

And you still wonder why you are not convincing and cannot attract newcomers to the language.

So, seriously - what's wrong with pointers in Rust?
My personal argument would be that their syntax and learning curve behind the involved idioms are making the code very difficult to comprehend. But this is the rational argument that was not mentioned here, you have instead stayed at the level of "curly braces are bad". Are there other rational arguments?

-- 
Maciej Sobczak * http://www.inspirel.com

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12 21:53             ` Randy Brukardt
@ 2019-03-13 10:50               ` Jere
  2019-03-17 12:52               ` Optikos
  2019-03-29 17:41               ` Florian Weimer
  2 siblings, 0 replies; 146+ messages in thread
From: Jere @ 2019-03-13 10:50 UTC (permalink / raw)


On Tuesday, March 12, 2019 at 5:53:04 PM UTC-4, Randy Brukardt wrote:
> 
> My understanding is that the SPARK people are far into designing ownership 
> contracts for Spark.
> 
> It's also possible that Ada 2020 will have a form of pointer ownership. 
> (Unfortunately, we didn't make any conclusions on that during yesterday's 
> meeting, so it's still in limbo, and we're getting very close to the finish 
> line.) 

Do you know if either group has been keeping up with the intended
implementations for both SPARK and Ada.  I noticed that from the FOSDEM
video that the SPARK version seemed to mimic the older version of the
Rust ownership/borrow method, but they have since upgraded it.  The 
older Rust version is more flexible than the accessibility levels
that Ada implements for named access types, using scope instead, but
the newer Rust version is "smarter" and actually looks at the actual 
lifetime of the reference instead of just the scope.

See Non-Lexical Lifetimes (odd name for the new system, but whatever):
https://blog.rust-lang.org/2018/12/06/Rust-1.31-and-rust-2018.html#non-lexical-lifetimes

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-13  9:10     ` Maciej Sobczak
@ 2019-03-13 11:08       ` Jere
  2019-03-13 11:11         ` Jere
  2019-03-13 11:59         ` Jere
  2019-03-13 13:44       ` Olivier Henley
  1 sibling, 2 replies; 146+ messages in thread
From: Jere @ 2019-03-13 11:08 UTC (permalink / raw)


On Wednesday, March 13, 2019 at 5:10:31 AM UTC-4, Maciej Sobczak wrote:
> OK, playing the devils's advocate again.
> 
> > As far as I can see, Rust's only innovation is safer pointers,
> 
> Which is, arguably, the innovation many people have been waiting for.
> 
> > but it still has 
> > a bad design that requires the use of pointers.
> 
> Why it is bad?
> Before, the criticism of pointers was based on the fact that pointers are dangerous. So, Ada is better, because it avoids these dangers.
> Now we have guys with *safe* pointers and what? They are bad, because they use pointers? And pointers are bad, because they are dange... wait, something's went wrong.

The harder sell of Jeff's argument is the same issue we constantly 
have heated discussions about in comp.lang.ada: proper terminology. 
Rust technically does have pointers, but they are not what Jeff is
talking about.  He's talking about references, which, technically,
not really pointers (they don't dangle, can't be freed, cannot be
shared, and aren't required to be implemented via pointers under 
the hood...though they probably are).  Trying to use a pointer in
Rust will net you a compiler error out of the box.  Rust's whole
mission is to discourage the use of pointers.

> And, surprise, nobody cares. Because now their pointers are safe.
> 
> > Other than that, Rust seems to be a typical C-family language with all the 
> > dangers that implies.
> 
> What dangers? Like for example pointers? Oh, wait...
> 
> And you still wonder why you are not convincing and cannot attract newcomers to the language.
> 

I just think in discussions like this, especially when they cross over into
other communities, shouldn't devolve into "you're wrong!", which can easily 
happen since many of us get pretty passionate about Ada.  Ada is the better
language overall, but if we go in too strongly and can't even use the 
terminology that Rust uses properly, then our arguments will just be ignored
and Ada doesn't get the advocacy it deserves.  We just end up looking like
zealots who cannot even research what we are talking about.  Note, that I
am not saying this has happened yet, but based on how the discussion is 
going in this email chain, if it were to spill over into the Rust thread, 
I would be concerned that it would happen.  I apologize if this sounds
accusatory.  I didn't intend it, but not sure how to write this out 
without it sounding that way.

That said, I think it would be bad for the Ada community to not appreciate
some of the good things that Rust does better than Ada.  They aren't many
and certainly aren't enough for me to think it is a better language, but
to blindly ignore them is a long term mistake for the community as a
whole as it only hurts Ada.  I think there is a lot to be gained if both
the Rust community and Ada community collaborated instead of competed, 
for both languages.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-13 11:08       ` Jere
@ 2019-03-13 11:11         ` Jere
  2019-03-13 11:59         ` Jere
  1 sibling, 0 replies; 146+ messages in thread
From: Jere @ 2019-03-13 11:11 UTC (permalink / raw)


On Wednesday, March 13, 2019 at 7:08:14 AM UTC-4, Jere wrote:
He's talking about references, which, technically,
> not really pointers (they don't dangle, can't be freed, cannot be
> shared
I meant cannot be shared as mutable 


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-13 11:08       ` Jere
  2019-03-13 11:11         ` Jere
@ 2019-03-13 11:59         ` Jere
  1 sibling, 0 replies; 146+ messages in thread
From: Jere @ 2019-03-13 11:59 UTC (permalink / raw)


On Wednesday, March 13, 2019 at 7:08:14 AM UTC-4, Jere wrote:
> 
> > And, surprise, nobody cares. Because now their pointers are safe.
> > 
> > > Other than that, Rust seems to be a typical C-family language with all the 
> > > dangers that implies.
> > 
> > What dangers? Like for example pointers? Oh, wait...
> > 
> > And you still wonder why you are not convincing and cannot attract newcomers to the language.
> > 
> 
> I just think in discussions like this, especially when they cross over into
> other communities, shouldn't devolve into "you're wrong!", which can easily 
> happen since many of us get pretty passionate about Ada.  
Just wanted to clarify, Maciej, that my response here isn't directly to
your quote, but to the email chain as a whole.  Your input just happened to
be the most recent discussion.  I too am worried about attracting new comers.
I wasn't intending to say your comments that I quoted fell into the "you're 
wrong" category at all.  Sorry if I caused confusion.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-08 16:43 Olivier Henley
                   ` (2 preceding siblings ...)
  2019-03-11 15:34 ` Lucretia
@ 2019-03-13 13:23 ` Olivier Henley
  2019-03-22 11:10 ` Lucretia
  2019-04-01  7:28 ` gautier_niouzes
  5 siblings, 0 replies; 146+ messages in thread
From: Olivier Henley @ 2019-03-13 13:23 UTC (permalink / raw)


Thanks to those who brought 'material' to the discussion.

a. The Rust thread is now closed and we did not slide into a flame war. Very good.

b. We definitely enlightened a whole bunch. You have no idea how many Rustaceans do not even know Ada exists. After all, awareness and politics are important. Very good.

c. From Randy's post, I find it exciting to see that this 'episode' is of actuality regarding Ada202X. Very good.

Thx



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-13  9:10     ` Maciej Sobczak
  2019-03-13 11:08       ` Jere
@ 2019-03-13 13:44       ` Olivier Henley
  2019-03-13 15:56         ` Simon Wright
  2019-03-14 22:41         ` Randy Brukardt
  1 sibling, 2 replies; 146+ messages in thread
From: Olivier Henley @ 2019-03-13 13:44 UTC (permalink / raw)


On Wednesday, March 13, 2019 at 5:10:31 AM UTC-4, Maciej Sobczak wrote:
> So, seriously - what's wrong with pointers in Rust?

From that excerpt by Oliver Scherer (Rust compiler contributor), it looks like the ownership aspect that comes with them is a real improvement:

"The two (obviously not a good amount of datapoints) large scale refactorings in Ada software that I've been part of have resulted in horrible hacks where people just spammed protected and pragma everywhere to get stuff working and bug free. The protected injections are because it's nearly impossible to figure out which things are accessed by multiple tasks without SPARK and you end up with undefined behaviour if you accidentally have a shared access to an unprotected memory location. The pragmas were reconfiguring things like stack size or disabling compiler warnings without actually thinking about what these changes meant.

Refactorings in Rust on the other hand are (compile-time) guaranteed to be free of race conditions, no matter how crazy you move stuff around or create new parallelism. Additionally the ownership concept lead to many libraries typestate encoding their API which makes misusing them a near impossibility (at compile-time) while Ada mainly catches those misuses at runtime via exceptions."

> My personal argument would be that their syntax and learning curve behind the involved idioms are making the code very difficult to comprehend. But this is the rational argument that was not mentioned here

Right. I did mention the equivalent on the Rust forum: 

"I fail to understand how the requiring of such [implicit knowledge](http://squidarth.com/rc/rust/2018/05/31/rust-borrowing-and-ownership.html) to achieve so little is desirable in any production environment?" 

Personally I plan to read the 'The Book' to see if those idioms are really 'hinderers' but also to know more about Rust.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-13 13:44       ` Olivier Henley
@ 2019-03-13 15:56         ` Simon Wright
  2019-03-13 16:25           ` Olivier Henley
  2019-03-13 16:27           ` Olivier Henley
  2019-03-14 22:41         ` Randy Brukardt
  1 sibling, 2 replies; 146+ messages in thread
From: Simon Wright @ 2019-03-13 15:56 UTC (permalink / raw)


Olivier Henley <olivier.henley@gmail.com> writes:

> From that excerpt by Oliver Scherer (Rust compiler contributor), it
> looks like the ownership aspect that comes with them is a real
> improvement:

Which excerpt? or, if it's this one, where's it from?

> "The two (obviously not a good amount of datapoints) large scale
> refactorings in Ada software that I've been part of have resulted in
> horrible hacks where people just spammed protected and pragma
> everywhere to get stuff working and bug free. The protected injections
> are because it's nearly impossible to figure out which things are
> accessed by multiple tasks without SPARK and you end up with undefined
> behaviour if you accidentally have a shared access to an unprotected
> memory location. The pragmas were reconfiguring things like stack size
> or disabling compiler warnings without actually thinking about what
> these changes meant.

Getting the stack size right seems to be a reasonable thing to be
worried about. Randomly suppressing compiler warnings without
investigating them & fixing or getting sign-off is .. well.

As to the tasking & access to unprotected data, you have to agree if the
data is got at via accessors. Ada allows large objects to be passed via
reference even if the mode is in, so there is an access, just under the
hood. I'm sure the clever SPARK guys have thought of this! and they have
the Global aspect(s) too.

> Refactorings in Rust on the other hand are (compile-time) guaranteed
> to be free of race conditions, no matter how crazy you move stuff
> around or create new parallelism. Additionally the ownership concept
> lead to many libraries typestate encoding their API which makes
> misusing them a near impossibility (at compile-time) while Ada mainly
> catches those misuses at runtime via exceptions."

If you have as undisciplined a refactoring of a tasking application as
hinted at in the first para above, you're heading for trouble regardless
of the language (IMO, of course). But not having even the possibility of
data trampling must be good!

People do have trouble understanding task safety. You can say of a
library "this [xxx] is not task-safe", but then they go and access it
from multiple tasks anyway. So you arrange that concurrent read-only
access is OK - and it turns out that they are modifying the thing from
another (set of) tasks at the same time!

I googled typestate encoding, the description at [1] leaves me a bit
baffled, as well as wondering whether the Rust guys find Ada syntax and
style as puzzling as theirs does me. However! I see that my link is to
embedded Rust, clearly I ought to look at that.

[1] https://rust-embedded.github.io/book/static-guarantees/typestate-programming.html

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-13 15:56         ` Simon Wright
@ 2019-03-13 16:25           ` Olivier Henley
  2019-03-14  0:40             ` Simon Wright
  2019-03-13 16:27           ` Olivier Henley
  1 sibling, 1 reply; 146+ messages in thread
From: Olivier Henley @ 2019-03-13 16:25 UTC (permalink / raw)


On Wednesday, March 13, 2019 at 11:56:13 AM UTC-4, Simon Wright wrote:
> Olivier Henley <olivier.henley@gmail.com> writes:
> 
> > From that excerpt by Oliver Scherer (Rust compiler contributor), it
> > looks like the ownership aspect that comes with them is a real
> > improvement:
> 
> Which excerpt? or, if it's this one, where's it from?
> 

https://www.reddit.com/r/ada/comments/7wzrqi/why_rust_was_the_best_thing_that_could_have/

second post by oli-obk... something like that. I find no anchor to reference it here properly.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-13 15:56         ` Simon Wright
  2019-03-13 16:25           ` Olivier Henley
@ 2019-03-13 16:27           ` Olivier Henley
  1 sibling, 0 replies; 146+ messages in thread
From: Olivier Henley @ 2019-03-13 16:27 UTC (permalink / raw)


On Wednesday, March 13, 2019 at 11:56:13 AM UTC-4, Simon Wright wrote:
> Which excerpt? or, if it's this one, where's it from?

https://www.reddit.com/r/ada/comments/7wzrqi/why_rust_was_the_best_thing_that_could_have/ 

second post by oli-obk... something like that. I find no anchor to reference it here properly. 


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-13 16:25           ` Olivier Henley
@ 2019-03-14  0:40             ` Simon Wright
  0 siblings, 0 replies; 146+ messages in thread
From: Simon Wright @ 2019-03-14  0:40 UTC (permalink / raw)


Olivier Henley <olivier.henley@gmail.com> writes:

> On Wednesday, March 13, 2019 at 11:56:13 AM UTC-4, Simon Wright wrote:
>> Olivier Henley <olivier.henley@gmail.com> writes:
>> 
>> > From that excerpt by Oliver Scherer (Rust compiler contributor), it
>> > looks like the ownership aspect that comes with them is a real
>> > improvement:
>> 
>> Which excerpt? or, if it's this one, where's it from?
>> 
>
> https://www.reddit.com/r/ada/comments/7wzrqi/why_rust_was_the_best_thing_that_could_have/
>
> second post by oli-obk... something like that. I find no anchor to
> reference it here properly.

That is a very fine thread.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-13 13:44       ` Olivier Henley
  2019-03-13 15:56         ` Simon Wright
@ 2019-03-14 22:41         ` Randy Brukardt
  2019-03-16 21:30           ` Olivier Henley
  1 sibling, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-14 22:41 UTC (permalink / raw)


"Olivier Henley" <olivier.henley@gmail.com> wrote in message 
news:b5b45418-4773-4768-89aa-f72f22da2e6e@googlegroups.com...
On Wednesday, March 13, 2019 at 5:10:31 AM UTC-4, Maciej Sobczak wrote:
>> So, seriously - what's wrong with pointers in Rust?

>From that excerpt by Oliver Scherer (Rust compiler contributor), it looks 
>like
>the ownership aspect that comes with them is a real improvement:
>
>"The two (obviously not a good amount of datapoints) large scale 
>refactorings
>in Ada software that I've been part of have resulted in horrible hacks 
>where
>people just spammed protected and pragma everywhere to get stuff working
>and bug free. The protected injections are because it's nearly impossible 
>to
>figure out which things are accessed by multiple tasks without SPARK and
>you end up with undefined behaviour if you accidentally have a shared 
>access
>to an unprotected memory location. The pragmas were reconfiguring things
>like stack size or disabling compiler warnings without actually thinking 
>about
>what these changes meant.

Obviously, if your existing code isn't documented properly as to what needs 
to be task-safe, then refactoring it isn't going to work very well. 
Refactoring bad code is just going to give you bad code. :-) And almost all 
code in any language is bad code, because at some point people turned to 
"just make it work" mode, and stopped doing the things necessary for the 
code to be understandable. Using Ada helps, but surely doesn't eliminate 
this point.

In any case, Ada 2020 is very much about addressing this point. The new 
Nonblocking and Global contracts make is possible to declare tasking and 
memory side-effects, and the "conflict check policies" allow using that to 
prevent data races. (Note that there is a difference between a "data race", 
and "race conditions"; there are plenty of race conditions that aren't data 
races, and no programming language can statically prevent the latter, since 
they're caused of a sequence of operations. Well, other than not having any 
task interactions in the first place. :-)

In addition, conflict checks are enabled by default on the new parallel 
constructs, so you have to work at causing problems. (The parallel 
constructs are safer anyway, since they do not allow blocking, so there 
aren't any rendezvous and entry calls to worry about.) And they can be 
enabled on tasks as well (not done by default for the obvious reason of 
compatibility - but also for capability, tasks should mainly be used in Ada 
2020 when one needs rendezvous and other contructs that can't be checked at 
compile-time).

The issue with this is that a dereference of an access value is almost 
always going to cause a conflict and thus be illegal. And the contracts for 
the containers are designed so that they can be used in parallel operations 
(presuming the actual parameters to the instance allow that). This means 
that no access types can be used to implement the containers, which is 
nonsense for the unbounded and indefinite containers. The ownership stuff is 
a proposal to limit that in the case of building ADTs, including the 
containers.

                                Randy.




^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-14 22:41         ` Randy Brukardt
@ 2019-03-16 21:30           ` Olivier Henley
  0 siblings, 0 replies; 146+ messages in thread
From: Olivier Henley @ 2019-03-16 21:30 UTC (permalink / raw)


>                                 Randy.

Thx for taking the time to develop on this. Really appreciated.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12 21:53             ` Randy Brukardt
  2019-03-13 10:50               ` Jere
@ 2019-03-17 12:52               ` Optikos
  2019-03-17 16:37                 ` Luke A. Guest
                                   ` (2 more replies)
  2019-03-29 17:41               ` Florian Weimer
  2 siblings, 3 replies; 146+ messages in thread
From: Optikos @ 2019-03-17 12:52 UTC (permalink / raw)


On Tuesday, March 12, 2019 at 5:53:04 PM UTC-4, Randy Brukardt wrote:
> "Lucretia" wrote in message 
> news:bba8f6a8-36ce-4bed-bd84-8a9ea7dc02f7@googlegroups.com...
> > On Tuesday, 12 March 2019 18:14:04 UTC, Olivier Henley  wrote:
> >> On Tuesday, March 12, 2019 at 12:32:34 PM UTC-4, Jeffrey R. Carter wrote:
> ...
> >> It has nothing to do with ourselves... me my, my.
> >>
> >> I suppose we did so to set the record straight about Ada to a community
> >> that has 'A LOT' of traction and think they are reinventing the wheel... 
> >> by staying blind to Ada.
> >
> > It's also to do with the fact that Rust isn't all that either. It 
> > literally only adds the
> > pointer ownership thing, nothing else, yet this is the hype this train is 
> > carrying and
> >  lods of people are getting on it, instead of getting on Ada.
> 
> My understanding is that the SPARK people are far into designing ownership 
> contracts for Spark.
> 
> It's also possible that Ada 2020 will have a form of pointer ownership. 
> (Unfortunately, we didn't make any conclusions on that during yesterday's 
> meeting, so it's still in limbo, and we're getting very close to the finish 
> line.) The current problem is that in Ada 2020 as it stands, it's not 
> possible to write a containers implementation in pure Ada. You'd have to 
> have some implementation hack to turn off some of the Legality Rules. Tucker 
> has designed a solution, based on an ownership mechanism, but as it is new 
> and barely vetted, it's unclear what we will do with it ultimately. Note 
> that this solution will not provide the perfect safety that you would get 
> with SPARK or Rust, but it would form the foundation of the SPARK solution 
> and it would clearly catch a lot of issues with using pointers to implement 
> ADTs. (And there is little other reason to use pointers, IMHO.)

I am sorry to hear that the hope for Ada being the 2nd language (not counting the Draconian SPARK variant) to achieve Rust's level of pointer safety has been abandoned.  ARG, please leave an immense paper trail of what-conflicts-with-what in Ada as defined to achieve a Rust-esque borrow checker in its full perfect-pointer form.

Randy, would Tucker's new ownership proposal come close to 100% feature-parity with Rust's borrow checker?  If not, then with or without Tucker's new ownership proposal, please provide an example of bad access code that Ada2020 would still allow to be written (e.g., a leak at runtime?) that Rust's borrow checker would find at compile-time.

Or equivalently (I think), technically what in today's Ada (or new in Ada2020) stops ARG from a wholesale importation of Rust's borrow checker grafted onto Ada syntax?  And why cannot the ARG apply for a timeline extension to ISO?  (If ever there was a time to have time to get it right, this would be the one!)

Ada being 2nd best at compile-time revelation of aberrant accesses/pointers with Rust being in 1st place does not market Ada well.  It makes it sound like Rust definitively won, despite Ada's 40 years of diligently trying to be the safest language.  (Let's not allow that to happen, or else the world needs AdaSyntaxRustSemantics as a new language—with a catchier name.)

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-17 12:52               ` Optikos
@ 2019-03-17 16:37                 ` Luke A. Guest
  2019-03-17 16:48                 ` Paul Rubin
  2019-03-18 23:36                 ` Randy Brukardt
  2 siblings, 0 replies; 146+ messages in thread
From: Luke A. Guest @ 2019-03-17 16:37 UTC (permalink / raw)


Optikos <optikos@verizon.net> wrote:


> Ada being 2nd best at compile-time revelation of aberrant
> accesses/pointers with Rust being in 1st place does not market Ada well. 
> It makes it sound like Rust definitively won, despite Ada's 40 years of
> diligently trying to be the safest language.  (Let's not allow that to
> happen, or else the world needs AdaSyntaxRustSemantics as a new
> language—with a catchier name.)
> 


This is something I’ve been thinking about, but one step further, no
pointers at all, it is possible.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-17 12:52               ` Optikos
  2019-03-17 16:37                 ` Luke A. Guest
@ 2019-03-17 16:48                 ` Paul Rubin
  2019-03-20  0:49                   ` Optikos
  2019-03-18 23:36                 ` Randy Brukardt
  2 siblings, 1 reply; 146+ messages in thread
From: Paul Rubin @ 2019-03-17 16:48 UTC (permalink / raw)


Optikos <optikos@verizon.net> writes:
> I am sorry to hear that the hope for Ada being the 2nd language (not
> counting the Draconian SPARK variant) to achieve Rust's level of
> pointer safety has been abandoned.

http://www.ats-lang.org/ ?

> ...  Rust definitively won ... the world needs AdaSyntaxRustSemantics
> as a new language—with a catchier name.)

More like the other way around--syntax is superficial and Rust's
C-descended style is more popular these days.  But Ada still has many
semantic advantages.  Safe pointers do seem like a good thing to import
from Rust.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-17 12:52               ` Optikos
  2019-03-17 16:37                 ` Luke A. Guest
  2019-03-17 16:48                 ` Paul Rubin
@ 2019-03-18 23:36                 ` Randy Brukardt
  2019-03-19  2:18                   ` Optikos
  2019-03-29 17:56                   ` Florian Weimer
  2 siblings, 2 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-03-18 23:36 UTC (permalink / raw)


"Optikos" <optikos@verizon.net> wrote in message 
news:6e1977a5-701e-4b4f-a937-a1b89d9127f0@googlegroups.com...
On Tuesday, March 12, 2019 at 5:53:04 PM UTC-4, Randy Brukardt wrote:
>ARG, please leave an immense paper trail of what-conflicts-with-what in
>Ada as defined to achieve a Rust-esque borrow checker in its full 
>perfect-pointer form.

Read the proposals for AI12-0240-1 through AI12-0240-5. The main problem is 
massive amounts of complexity.

>Randy, would Tucker's new ownership proposal come close to 100% 
>feature-parity
>with Rust's borrow checker?

Surely not the latest one, since lots of stuff was dropped from it.

But a better question is whether the Rust borrow checker allows building 
proper ADTs for most data structures. Most of Tucker's proposals didn't have 
a safe way to build typical data structures like a doubly-linked list or the 
parent pointer of a tree structure. Leaving out these backward pointers 
means adding a substantial performance degradation for (possibly) common 
operations like node deletion. Depending on what you're doing, that could be 
a non-starter. I haven't had a chance to actually look at Rust's actual 
rules; Ada is hard enough and as we're in the home stretch for Ada 2020, I 
literally don't have time for much else. (Probably shouldn't be answering 
this message...)

Tucker's latest proposal does address the back pointer problem. So at least 
that can be done with checks.

In any case, an Ada proposal has to be able to build the containers, and 
since the containers are designed with possibly dangling cursors, a totally 
safe system would not be usable with them. The containers do include checks 
that would detect many ownership problems, however, so any lack of 
compile-time safety is definitely mitigated. (It's not 100% safe because of 
the possiblity that a cursor outlive the owner object; in that case, the 
checks are unreliable.)

                          Randy.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-18 23:36                 ` Randy Brukardt
@ 2019-03-19  2:18                   ` Optikos
  2019-03-19  8:44                     ` Dmitry A. Kazakov
  2019-03-19  9:37                     ` Optikos
  2019-03-29 17:56                   ` Florian Weimer
  1 sibling, 2 replies; 146+ messages in thread
From: Optikos @ 2019-03-19  2:18 UTC (permalink / raw)


On Monday, March 18, 2019 at 7:36:17 PM UTC-4, Randy Brukardt wrote:
> "Optikos" wrote in message 
> news:6e1977a5-701e-4b4f-a937-a1b89d9127f0@googlegroups.com...
> On Tuesday, March 12, 2019 at 5:53:04 PM UTC-4, Randy Brukardt wrote:
> >ARG, please leave an immense paper trail of what-conflicts-with-what in
> >Ada as defined to achieve a Rust-esque borrow checker in its full 
> >perfect-pointer form.
> 
> Read the proposals for AI12-0240-1 through AI12-0240-5. The main problem is 
> massive amounts of complexity.
> 
> >Randy, would Tucker's new ownership proposal come close to 100% 
> >feature-parity
> >with Rust's borrow checker?
> ...
> since the containers are designed with possibly dangling cursors, a totally 
> safe system would not be usable with them. The containers do include checks 
> that would detect many ownership problems, however, so any lack of 
> compile-time safety is definitely mitigated. (It's not 100% safe because of 
> the possiblity that a cursor outlive the owner object; in that case, the 
> checks are unreliable.)

A container could have (as a required fundamental axiom) a singly-linked list of spirits of all cursors ever created that reference it.  As each cursor's life ends, that dying cursor directly knows O(1) where its spirit is within that linked list, and then removes its dying spirit too.  Then as the lifetime of the container ends, the finalization of that linked list is to walk that link-list of spirits to abruptly undermine each spirit's corresponding still-living cursor so that that longer-lived-than-its-container cursor abruptly has the usual customary representation of cursor-exhausted-its-walk-of-the-container (i.e., the end-of-loop criterion during normal-operations' not-end-of-lifed cursor walks of not-end-of-lifed container), so that cursors are all instantly loop-terminating gracefully whenever their container ceases to exist.

Hence, no cursor ever contains a pointer/access/address value that out lives its container, because that pointer was overwritten (at container finalization) with the cursor-exhausted-its-walk-of-the-container reserved value that all loops & conditional branches interrogate as a matter of their normal-operations behavior.  Q.E.D.

Randy, are there any other examples of feared-to-be-dangling pointers outliving what they point to in Tucker's latest proposal?


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19  2:18                   ` Optikos
@ 2019-03-19  8:44                     ` Dmitry A. Kazakov
  2019-03-19  9:53                       ` Optikos
  2019-03-19 22:04                       ` Randy Brukardt
  2019-03-19  9:37                     ` Optikos
  1 sibling, 2 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-19  8:44 UTC (permalink / raw)


On 2019-03-19 03:18, Optikos wrote:
> On Monday, March 18, 2019 at 7:36:17 PM UTC-4, Randy Brukardt wrote:

>> since the containers are designed with possibly dangling cursors, a totally
>> safe system would not be usable with them. The containers do include checks
>> that would detect many ownership problems, however, so any lack of
>> compile-time safety is definitely mitigated. (It's not 100% safe because of
>> the possiblity that a cursor outlive the owner object; in that case, the
>> checks are unreliable.)
> 
> A container could have (as a required fundamental axiom) a singly-linked list of spirits of all cursors ever created that reference it.  As each cursor's life ends, that dying cursor directly knows O(1) where its spirit is within that linked list, and then removes its dying spirit too.  Then as the lifetime of the container ends, the finalization of that linked list is to walk that link-list of spirits to abruptly undermine each spirit's corresponding still-living cursor so that that longer-lived-than-its-container cursor abruptly has the usual customary representation of cursor-exhausted-its-walk-of-the-container (i.e., the end-of-loop criterion during normal-operations' not-end-of-lifed cursor walks of not-end-of-lifed container), so that cursors are all instantly loop-terminating gracefully whenever their container ceases to exist.

Forgive my ignorance, but how this is different from a weak reference?

> Hence, no cursor ever contains a pointer/access/address value that out lives its container, because that pointer was overwritten (at container finalization) with the cursor-exhausted-its-walk-of-the-container reserved value that all loops & conditional branches interrogate as a matter of their normal-operations behavior.  Q.E.D.

The cursor is still dangling. The difference is that one can check if it 
indeed is (with a nice race condition attached).

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19  2:18                   ` Optikos
  2019-03-19  8:44                     ` Dmitry A. Kazakov
@ 2019-03-19  9:37                     ` Optikos
  2019-03-19 22:21                       ` Randy Brukardt
  1 sibling, 1 reply; 146+ messages in thread
From: Optikos @ 2019-03-19  9:37 UTC (permalink / raw)


On Monday, March 18, 2019 at 10:18:54 PM UTC-4, Optikos wrote:
> On Monday, March 18, 2019 at 7:36:17 PM UTC-4, Randy Brukardt wrote:
> > "Optikos" wrote in message 
> > news:6e1977a5-701e-4b4f-a937-a1b89d9127f0@googlegroups.com...
> > On Tuesday, March 12, 2019 at 5:53:04 PM UTC-4, Randy Brukardt wrote:
> > >ARG, please leave an immense paper trail of what-conflicts-with-what in
> > >Ada as defined to achieve a Rust-esque borrow checker in its full 
> > >perfect-pointer form.
> > 
> > Read the proposals for AI12-0240-1 through AI12-0240-5. The main problem is 
> > massive amounts of complexity.
> > 
> > >Randy, would Tucker's new ownership proposal come close to 100% 
> > >feature-parity
> > >with Rust's borrow checker?
> > ...
> > since the containers are designed with possibly dangling cursors, a totally 
> > safe system would not be usable with them. The containers do include checks 
> > that would detect many ownership problems, however, so any lack of 
> > compile-time safety is definitely mitigated. (It's not 100% safe because of 
> > the possiblity that a cursor outlive the owner object; in that case, the 
> > checks are unreliable.)
> 
> A container could have (as a required fundamental axiom) a singly-linked list of spirits of all cursors ever created that reference it.  As each cursor's life ends, that dying cursor directly knows O(1) where its spirit is within that linked list, and then removes its dying spirit too.  Then as the lifetime of the container ends, the finalization of that linked list is to walk that link-list of spirits to abruptly undermine each spirit's corresponding still-living cursor so that that longer-lived-than-its-container cursor abruptly has the usual customary representation of cursor-exhausted-its-walk-of-the-container (i.e., the end-of-loop criterion during normal-operations' not-end-of-lifed cursor walks of not-end-of-lifed container), so that cursors are all instantly loop-terminating gracefully whenever their container ceases to exist.
> 
> Hence, no cursor ever contains a pointer/access/address value that out lives its container, because that pointer was overwritten (at container finalization) with the cursor-exhausted-its-walk-of-the-container reserved value that all loops & conditional branches interrogate as a matter of their normal-operations behavior.  Q.E.D.
> 
> Randy, are there any other examples of feared-to-be-dangling pointers outliving what they point to in Tucker's latest proposal?

I was combining memories of 2 prior designs as I wrote this.  That “singly-linked list” should have been:  doubly linked list.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19  8:44                     ` Dmitry A. Kazakov
@ 2019-03-19  9:53                       ` Optikos
  2019-03-19 22:13                         ` Randy Brukardt
  2019-03-19 22:04                       ` Randy Brukardt
  1 sibling, 1 reply; 146+ messages in thread
From: Optikos @ 2019-03-19  9:53 UTC (permalink / raw)


On Tuesday, March 19, 2019 at 4:44:16 AM UTC-4, Dmitry A. Kazakov wrote:
> On 2019-03-19 03:18, Optikos wrote:
> > On Monday, March 18, 2019 at 7:36:17 PM UTC-4, Randy Brukardt wrote:
> 
> >> since the containers are designed with possibly dangling cursors, a totally
> >> safe system would not be usable with them. The containers do include checks
> >> that would detect many ownership problems, however, so any lack of
> >> compile-time safety is definitely mitigated. (It's not 100% safe because of
> >> the possiblity that a cursor outlive the owner object; in that case, the
> >> checks are unreliable.)
> > 
> > A container could have (as a required fundamental axiom) a singly-linked list of spirits of all cursors ever created that reference it.  As each cursor's life ends, that dying cursor directly knows O(1) where its spirit is within that linked list, and then removes its dying spirit too.  Then as the lifetime of the container ends, the finalization of that linked list is to walk that link-list of spirits to abruptly undermine each spirit's corresponding still-living cursor so that that longer-lived-than-its-container cursor abruptly has the usual customary representation of cursor-exhausted-its-walk-of-the-container (i.e., the end-of-loop criterion during normal-operations' not-end-of-lifed cursor walks of not-end-of-lifed container), so that cursors are all instantly loop-terminating gracefully whenever their container ceases to exist.
> 
> Forgive my ignorance, but how this is different from a weak reference?

What part of ‘container contains a doubly-linked list of spirit pointers to all cursors of that container’ and ‘each cursor contains a pointer back to its spirit’ did you not deeply grok?  (Go back and study it some more.)  Weak-reference smart pointers have none of that spirit stuff, hence why I explain its internal interplay so that each reader can see its purpose.  Forgive my ignorance, but how is a farm tractor different than the Moon?

> > Hence, no cursor ever contains a pointer/access/address value that out lives its container, because that pointer was overwritten (at container finalization) with the cursor-exhausted-its-walk-of-the-container reserved value that all loops & conditional branches interrogate as a matter of their normal-operations behavior.  Q.E.D.
> 
> The cursor is still dangling. The difference is that one can check if it 
> indeed is 

Absolutely not.  The cursor cannot dangle after the finalization of the container.  No dangling after container-finalization means no dangling-of-cursor at all. Q.E.D.

> (with a nice race condition attached)

(sigh) Spoil all of the container's cursors (via the walk of the doubly-linked list of spirits) prior to dismantling the contents of the container.  This would need to be lock-free (e.g., CMOV in x86) data structures, but then again so did multithreaded access to the container.  If you bash how to make the spirit doubly-linked list efficiently thread-safe, then I can turn it around on you to bash the analogous topic with multithreaded manipulations of a container that is being finalized by another thread.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19  8:44                     ` Dmitry A. Kazakov
  2019-03-19  9:53                       ` Optikos
@ 2019-03-19 22:04                       ` Randy Brukardt
  2019-03-19 22:22                         ` Paul Rubin
  1 sibling, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-19 22:04 UTC (permalink / raw)


"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:q6qa4u$kd0$1@gioia.aioe.org...
> On 2019-03-19 03:18, Optikos wrote:
>> On Monday, March 18, 2019 at 7:36:17 PM UTC-4, Randy Brukardt wrote:
>
>>> since the containers are designed with possibly dangling cursors, a 
>>> totally
>>> safe system would not be usable with them. The containers do include 
>>> checks
>>> that would detect many ownership problems, however, so any lack of
>>> compile-time safety is definitely mitigated. (It's not 100% safe because 
>>> of
>>> the possiblity that a cursor outlive the owner object; in that case, the
>>> checks are unreliable.)
>>
>> A container could have (as a required fundamental axiom) a singly-linked 
>> list of spirits of all cursors ever created that reference it.  As each 
>> cursor's life ends, that dying cursor directly knows O(1) where its 
>> spirit is within that linked list, and then removes its dying spirit too. 
>> Then as the lifetime of the container ends, the finalization of that 
>> linked list is to walk that link-list of spirits to abruptly undermine 
>> each spirit's corresponding still-living cursor so that that 
>> longer-lived-than-its-container cursor abruptly has the usual customary 
>> representation of cursor-exhausted-its-walk-of-the-container (i.e., the 
>> end-of-loop criterion during normal-operations' not-end-of-lifed cursor 
>> walks of not-end-of-lifed container), so that cursors are all instantly 
>> loop-terminating gracefully whenever their container ceases to exist.
>
> Forgive my ignorance, but how this is different from a weak reference?
>
>> Hence, no cursor ever contains a pointer/access/address value that out 
>> lives its container, because that pointer was overwritten (at container 
>> finalization) with the cursor-exhausted-its-walk-of-the-container 
>> reserved value that all loops & conditional branches interrogate as a 
>> matter of their normal-operations behavior.  Q.E.D.
>
> The cursor is still dangling. The difference is that one can check if it 
> indeed is (with a nice race condition attached).

Right. And dangling pointers are illegal in a full Rust-like scheme. So you 
can't declare them at all, which is a problem when you need to implement an 
existing specification that has them.

A lot of what the ownership scheme does well isn't really necessary in Ada 
in the first place, as one can use a discriminant-dependent component to get 
the same effect without any pointers at all. I'm talking about 
dynamically-sized arrays and singly-linked lists (which are just sequences 
of elements, can be modeled as an array just as well as with a list). The 
more complex data strurtures seem to be very hard to build that way -- but 
those are the only ones really need pointers in the first place. So I'm not 
fully sold on the concept as the cure to all ills - it's just another tool 
to make code a bit safer.

                       Randy.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19  9:53                       ` Optikos
@ 2019-03-19 22:13                         ` Randy Brukardt
  2019-03-19 22:26                           ` Paul Rubin
                                             ` (2 more replies)
  0 siblings, 3 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-03-19 22:13 UTC (permalink / raw)


"Optikos" <optikos@verizon.net> wrote in message 
news:f4eee526-e607-4e1f-843f-9913c9c093f9@googlegroups.com...
...
>Absolutely not.  The cursor cannot dangle after the finalization of the 
>container.
>No dangling after container-finalization means no dangling-of-cursor at 
>all. Q.E.D.

Baloney. The cursor object still exists, and someone can still try to use 
it. Yes, you'll get an exception rather than erroneous execution, but it is 
still dangling (the term in the RM for cursors is "invalid"). (And note that 
there are cheaper ways to get that effect.)

The whole point of the Rust scheme as I understand it is to avoid such 
things. In particular, you can never have a pointer with multiple owners. 
The "borrow" scheme as I understand it allows the owner to be temporarily 
transfered (so you can walk lists, for instance), but long-term storage of 
such pointers is simply not allowed. You can't build a cursor that way (nor 
a doubly-linked list). Perhaps the Rust people have gone beyond simple 
borrow semantics -- I don't know.

Tucker's latest proposal lets one build cursors, but it can't detect changes 
where the owner of a node is changed after the fact (think of an operation 
like a list Splice where nodes are moved from one list to another). To do 
that would require putting a lot of restrictions on how an ADT is used, 
again something that cannot be done with the existing containers (and it's 
unclear that that is a good idea anyway, since it is leaking implementation 
characteristics to usages).

                           Randy.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19  9:37                     ` Optikos
@ 2019-03-19 22:21                       ` Randy Brukardt
  0 siblings, 0 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-03-19 22:21 UTC (permalink / raw)


"Optikos" <optikos@verizon.net> wrote in message 
news:aa13d9dd-69e9-48ac-99d0-3fabef216781@googlegroups.com...
...
> A container could have (as a required fundamental axiom) a singly-linked
>list of spirits of all cursors ever created that reference it.

Matt suggested such an implementation when the containers were designed. But 
only for deep testing, because...

>As each cursor's life ends, that dying cursor directly knows O(1) where its
>spirit is within that linked list, and then removes its dying spirit too.

This means that each cursor has to be controlled (explicitly or with 
something that is effectively the same), and that means that cursor 
operations are going to be much more expensive. Particularly operations that 
return cursors from functions. (Those are probably 10x slower.) And since 
iterations are built on a bunch of such functions, it too would be much 
slower.

I don't think anyone would accept the Ada containers if they are 
intentionally that slow by design. (The place where that was true in Ada 
2012 has spawned a lot of revision in Ada 2020, it would be madness to put 
it back somewhere else.)

                                                 Randy.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19 22:04                       ` Randy Brukardt
@ 2019-03-19 22:22                         ` Paul Rubin
  2019-03-19 23:01                           ` Randy Brukardt
  0 siblings, 1 reply; 146+ messages in thread
From: Paul Rubin @ 2019-03-19 22:22 UTC (permalink / raw)


"Randy Brukardt" <randy@rrsoftware.com> writes:
> A lot of what the ownership scheme does well isn't really necessary in
> Ada in the first place, as one can use a discriminant-dependent
> component to get the same effect without any pointers at all.

Does that mean just some kind of tagged record?  Of course that would
work the same way in other languages, maybe with different surface
syntax.

> and singly-linked lists (which are just sequences of elements, can be
> modeled as an array just as well as with a list).

I think that's not so easy: a common practice with linked lists is to
have multiple lists with different heads sharing the same tail.  So
there has to be some indirection.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19 22:13                         ` Randy Brukardt
@ 2019-03-19 22:26                           ` Paul Rubin
  2019-03-20  1:08                             ` Jere
  2019-03-19 22:36                           ` Optikos
  2019-03-20  1:20                           ` Jere
  2 siblings, 1 reply; 146+ messages in thread
From: Paul Rubin @ 2019-03-19 22:26 UTC (permalink / raw)


"Randy Brukardt" <randy@rrsoftware.com> writes:
> Rust...  You can't build a cursor that way (nor a doubly-linked
> list). Perhaps the Rust people have gone beyond simple borrow
> semantics -- I don't know.

I did a little web searching and it does seem to me that as of a year or
so ago, the way to make doubly linked lists in Rust was to call some
kind of unchecked library.  I'd like to know how it's done in ATS, and
I might ask on a Rust chat if it's still like that in Rust.

I think it might be a serious issue for Rust, since one of Rust's
driving applications was web browsers.  Those build DOM trees where
nodes point to both their children and their parent, so the tree is full
of cycles.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19 22:13                         ` Randy Brukardt
  2019-03-19 22:26                           ` Paul Rubin
@ 2019-03-19 22:36                           ` Optikos
  2019-03-19 23:13                             ` Randy Brukardt
  2019-03-20  1:20                           ` Jere
  2 siblings, 1 reply; 146+ messages in thread
From: Optikos @ 2019-03-19 22:36 UTC (permalink / raw)


On Tuesday, March 19, 2019 at 6:13:20 PM UTC-4, Randy Brukardt wrote:
> "Optikos" wrote in message 
> news:f4eee526-e607-4e1f-843f-9913c9c093f9@googlegroups.com...
> ...
> >Absolutely not.  The cursor cannot dangle after the finalization of the 
> >container.
> >No dangling after container-finalization means no dangling-of-cursor at 
> >all. Q.E.D.
> 
> Baloney. The cursor object still exists, and someone can still try to use 
> it. Yes, you'll get an •••exception••• rather than erroneous execution

No, you have it all wrong •••there•••.  Not raise an exception, but rather gracefully take the end-of-walk branch of code, just as in normal operations.  Nothing exceptional about it.  Cursors have as their fundamental mission to walk a (portion of a) container until the end-of-walk conditional branch is taken instead, meaning that the walk reached its natural terminus.  No raise.  No exception.  Nothing aberrant.  Just end of the walk.  Just
1) the else branch taken instead of the then branch
or
2) exit loop taken instead of another iteration.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19 22:22                         ` Paul Rubin
@ 2019-03-19 23:01                           ` Randy Brukardt
  0 siblings, 0 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-03-19 23:01 UTC (permalink / raw)


"Paul Rubin" <no.email@nospam.invalid> wrote in message 
news:874l7y4i7x.fsf@nightsong.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>> A lot of what the ownership scheme does well isn't really necessary in
>> Ada in the first place, as one can use a discriminant-dependent
>> component to get the same effect without any pointers at all.
>
> Does that mean just some kind of tagged record?  Of course that would
> work the same way in other languages, maybe with different surface
> syntax.

No, I just mean a discriminanted record:

    subtype Short_Natural range 0 .. 100;
    type Short_List is (Len : Short_Natural := 0) is record
          Data : array (1 .. Len) of Element_Type;
    end record;

Depending on the implementation, there might be no pointers at all in the 
implementation, or there might be some hidden ones that are handled 
automatically. Either way, there is no exposed pointers and thus no danger 
associated with them.

One has to assign this as a whole, but that's usually easy. Janus/Ada has a 
lot of tiny linked lists that could probably have been done this way (and 
would be safer, but a bit less control over memory management).

>> and singly-linked lists (which are just sequences of elements, can be
>> modeled as an array just as well as with a list).
>
> I think that's not so easy: a common practice with linked lists is to
> have multiple lists with different heads sharing the same tail.  So
> there has to be some indirection.

True, but you (probably) can't do that in Rust anyway.

Some background here: The basic idea behind pointer ownership is to prevent 
various issues by enforcing an invariant -- that each allocated object is 
stored in exactly one pointer object. This is enforced with a variety of 
runtime and compile-time rules.

Now, it's clear that one can't even walk a data structure that way, so the 
idea of "borrowing" a pointer for a limited time was invented. Such 
borrowing has to be done in carefully controlled ways in order to keep it 
being safe -- for instance, no one can read or write the original pointer 
while it is borrowed.

Multiple long-lived pointers that point at a single object are simply not 
allowed. In part, that's done by making assignment either illegal or a move 
(where the source is nulled when the pointer is assigned).

For something like a cursor, that means that Rust-pointers couldn't be used 
to create the object. The entire point of a cursor is that it is a 
long-lived handle to a specific element in a larger data structure. One 
can't null out part of the data structure to create the handle, and if the 
assignment is banned completely, you could never create a valid cursor 
object in the first place.

There are similar issues with back pointers in a data structure, as you 
might guess.

                                 Randy.


                    Randy.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19 22:36                           ` Optikos
@ 2019-03-19 23:13                             ` Randy Brukardt
  2019-03-20  1:28                               ` Jere
  2019-03-20  7:59                               ` Optikos
  0 siblings, 2 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-03-19 23:13 UTC (permalink / raw)


"Optikos" <optikos@verizon.net> wrote in message 
news:de2f5462-fa10-4fdf-97a6-99989e40c697@googlegroups.com...
On Tuesday, March 19, 2019 at 6:13:20 PM UTC-4, Randy Brukardt wrote:
>> Baloney. The cursor object still exists, and someone can still try to use
>> it. Yes, you'll get an ...exception... rather than erroneous execution
>
>No, you have it all wrong ...there....  Not raise an exception, but rather
>gracefully take the end-of-walk branch of code, just as in normal 
>operations.

Walking is only a small portion of the usage of cursors, and IMHO it is the 
least important one (since everyone other than container developers ought to 
be using iterators to walk their containers).

A cursor is a handle accessing an element of a larger container, nothing 
more or less than that. The primary usage is to connect data structures made 
up of multiple containers. For instance, consider a compiler symboltable. 
There is a tree structure that represents each of the declarations and their 
scopes, and a map structure that represents a mapping of names to nodes of 
the treee. The contents of that map is going to be tree cursors, each 
representing a declaration with a particular name.

In such a structure, it would be common to assume that the cursors are valid 
(just like you would assume that pointers are non-null in such a case --  
that's precisely what Janus/Ada code does, for instance). And dereferencing 
a cursor that points at a deleted node has to raise some exception (just as 
it would when using a pointer).

The value of cursors is that they can be implemented by a range of 
abstractions with a range of checking, from array indicies (as in the 
bounded containers and the vector) to pointers with a variety of schemes 
from no dangling checking to the bulletproof controlled cursor scheme.

In any case, the implementation of a cursor is irrelevant, since the Rust 
scheme doesn't allow making copies of pointers in the first place. Since you 
can't create a cursor with a pointer implementation, it becomes irrelevant 
as to how it is treated at end-of-life.

Sadly, what I see here is someone who's so bought into Rust hype that they 
fail to consider the real trade-offs implicit in such a technology. There's 
no reason to bring the basic Rust scheme into Ada, since there is almost no 
reason in Ada to create such pointers in the first place (see my reply to 
Paul). Where everyone needs help is for complex data structures, and Rust 
(as I understand it, anyway) provides little help there. Tucker at least is 
trying to help with the issues associated with those sorts of structures, 
but it remains to be seen whether the proposal can get baked enough to get 
it into Ada 2020.

                            Randy.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-17 16:48                 ` Paul Rubin
@ 2019-03-20  0:49                   ` Optikos
  2019-03-20  1:04                     ` Paul Rubin
  0 siblings, 1 reply; 146+ messages in thread
From: Optikos @ 2019-03-20  0:49 UTC (permalink / raw)


On Sunday, March 17, 2019 at 12:49:00 PM UTC-4, Paul Rubin wrote:
> Optikos writes:
> > I am sorry to hear that the hope for Ada being the 2nd language (not
> > counting the Draconian SPARK variant) to achieve Rust's level of
> > pointer safety has been abandoned.
> 
> http://www.ats-lang.org/ ?

Paul, how similar or dissimilar to (SPARK + Ada) do you think (ATS's proof mode + ATS's programming mode) is?  My sense is that ATS is doing something substantially different than SPARK, but perhaps I need to look more deeply at ATS.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-20  0:49                   ` Optikos
@ 2019-03-20  1:04                     ` Paul Rubin
  2019-03-20  1:19                       ` Optikos
  0 siblings, 1 reply; 146+ messages in thread
From: Paul Rubin @ 2019-03-20  1:04 UTC (permalink / raw)


Optikos <optikos@verizon.net> writes:
> Paul, how similar or dissimilar to (SPARK + Ada) do you think (ATS's
> proof mode + ATS's programming mode) is?

Very very very different.  But I haven't used either one so I probably
can't give a better description than that.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19 22:26                           ` Paul Rubin
@ 2019-03-20  1:08                             ` Jere
  2019-03-22  2:26                               ` Randy Brukardt
  0 siblings, 1 reply; 146+ messages in thread
From: Jere @ 2019-03-20  1:08 UTC (permalink / raw)


On Tuesday, March 19, 2019 at 6:26:51 PM UTC-4, Paul Rubin wrote:
> "Randy Brukardt" writes:
> > Rust...  You can't build a cursor that way (nor a doubly-linked
> > list). Perhaps the Rust people have gone beyond simple borrow
> > semantics -- I don't know.
> 
> I did a little web searching and it does seem to me that as of a year or
> so ago, the way to make doubly linked lists in Rust was to call some
> kind of unchecked library.  I'd like to know how it's done in ATS, and
> I might ask on a Rust chat if it's still like that in Rust.
> 
> I think it might be a serious issue for Rust, since one of Rust's
> driving applications was web browsers.  Those build DOM trees where
> nodes point to both their children and their parent, so the tree is full
> of cycles.

If you need either doubly linked lists or maps in Rust, you use the 
ones provided by the standard library (std::collections::list, for
example, is the doubly linked list).  It's not unchecked at all.

If you want to roll your own doubly linked list, then you will need to
have to have a couple of "unsafe" calls (they don't really have 
libraries that are unchecked, mostly just traits and operations).
They are small conversions usually. It is similar to trying to implement
the standard containers in Ada where you may have to do 
unchecked_deallocations, unchecked_conversions, compiler specific
operations/attributes, etc. to implement things like tampering checks
and memory deallocation.

In both Rust and Ada you can restrict them to small localized sections.
The big difference really ends up being the ecosystems.  The Rust
community tends to lobotomize libraries with unnecessary unsafe calls
where the Ada community doesn't really have a centralized library
system that facilitate that.  Not that it couldn't.  

reference for the doubly linked list in standard rust (no unsafe calls):
https://doc.rust-lang.org/std/collections/struct.LinkedList.html

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-20  1:04                     ` Paul Rubin
@ 2019-03-20  1:19                       ` Optikos
  0 siblings, 0 replies; 146+ messages in thread
From: Optikos @ 2019-03-20  1:19 UTC (permalink / raw)


On Tuesday, March 19, 2019 at 9:04:04 PM UTC-4, Paul Rubin wrote:
> Optikos  writes:
> > Paul, how similar or dissimilar to (SPARK + Ada) do you think (ATS's
> > proof mode + ATS's programming mode) is?
> 
> Very very very different.

That was also my shallow-understanding initial-impression of ATS.  Thank you for this tip on ATS; your posts often are true gift of fresh interesting ideas.  (Even when I as a lurker disagree with you, I often enjoy pondering the mirror-image-of-your-idea that I do agree wholeheartedly with.)  I will investigate ATS much further.  It looks fascinating so far, but I really need to learn its syntax better to have full appreciation, I think.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19 22:13                         ` Randy Brukardt
  2019-03-19 22:26                           ` Paul Rubin
  2019-03-19 22:36                           ` Optikos
@ 2019-03-20  1:20                           ` Jere
  2019-03-22  2:30                             ` Randy Brukardt
  2 siblings, 1 reply; 146+ messages in thread
From: Jere @ 2019-03-20  1:20 UTC (permalink / raw)


On Tuesday, March 19, 2019 at 6:13:20 PM UTC-4, Randy Brukardt wrote:
> 
> The whole point of the Rust scheme as I understand it is to avoid such 
> things. In particular, you can never have a pointer with multiple owners. 
> The "borrow" scheme as I understand it allows the owner to be temporarily 
> transfered (so you can walk lists, for instance), but long-term storage of 
> such pointers is simply not allowed. You can't build a cursor that way (nor 
> a doubly-linked list). Perhaps the Rust people have gone beyond simple 
> borrow semantics -- I don't know.
> 
Rust has a couple levels of ownership and borrowing.  It employs both
spacial and temporal ownership rules.  The 90% solution uses spacial
rules (the ones you are most likely familiar with).  For managing
data across threads or doing complex data types, Rust also provides
temporal ownership/borrowing.  Think of the same distinction Ada has
for named access types vs anonymous access types. You can catch a lot
more at compile time with named access types, but anonymous access types
can potentially have more runtime checking.  In Rust, the standard reference
scheme you are probably familiar with employ spacial ownership.  If you
need temporal ownership, then for single threaded you use things like
the RC<> generic (reference counted), and for multi-threaded you use things
like the ARC<> generic (atomic reference counted).  There are other things
of similar nature.  These employ temporal rules, which can potentially 
require runtime checks, though the presence of the spacial ownership rules
can help optimize out a lot of the run time checks.  I kind of mentioned 
this above, but the spacial and temporal rules aren't mutually exclusive.
They can work together when needed.

I don't know if you saw my earlier question to you (from a while back in
this email chain), but do you know if Tucker was looking at the recent
upgrades to the ownership scheme?  Some of them may (or may not) be useful
for Ada (if that gets implemented).  In particular, in the old ownership
scheme, if you needed to use a throwaway variable to capture a return result
in Rust, you couldn't reborrow again until that throwaway variable went
out of scope.  In the updated system, they are able to tell it is throwaway
and allow for the ownership transfer.  I was thinking about this for
Ada particularly since we are required to capture function returns into
some sort of variable.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19 23:13                             ` Randy Brukardt
@ 2019-03-20  1:28                               ` Jere
  2019-03-20  8:42                                 ` Dmitry A. Kazakov
  2019-03-22  2:00                                 ` Randy Brukardt
  2019-03-20  7:59                               ` Optikos
  1 sibling, 2 replies; 146+ messages in thread
From: Jere @ 2019-03-20  1:28 UTC (permalink / raw)


On Tuesday, March 19, 2019 at 7:13:47 PM UTC-4, Randy Brukardt wrote:
> 
> Sadly, what I see here is someone who's so bought into Rust hype that they 
> fail to consider the real trade-offs implicit in such a technology. There's 
> no reason to bring the basic Rust scheme into Ada, since there is almost no 
> reason in Ada to create such pointers in the first place (see my reply to 
> Paul). 

I'd say the biggest area that forces me to use access types is when
dealing with complex limited types.  If I want to use any kind of container
implementation for a collection of limited types, I am forced to roll 
my own and generally have to use access types somewhere.  Same if I need
to use a limited type in non limited context.  Ada is generally very 
good about not requiring them, but there are gaps that could be filled.

You would think that a container of limited types would be very restrictive,
but with the advent of Implicit_Dereference and reference types, there
is definitely some meat there.  I would say maps and lists are the two 
areas I find the most need.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-19 23:13                             ` Randy Brukardt
  2019-03-20  1:28                               ` Jere
@ 2019-03-20  7:59                               ` Optikos
  2019-03-22  2:16                                 ` Randy Brukardt
  1 sibling, 1 reply; 146+ messages in thread
From: Optikos @ 2019-03-20  7:59 UTC (permalink / raw)


On Tuesday, March 19, 2019 at 7:13:47 PM UTC-4, Randy Brukardt wrote:
> "Optikos" wrote in message 
> news:de2f5462-fa10-4fdf-97a6-99989e40c697@googlegroups.com...
> On Tuesday, March 19, 2019 at 6:13:20 PM UTC-4, Randy Brukardt wrote:
> >> Baloney. The cursor object still exists, and someone can still try to use
> >> it. Yes, you'll get an ...exception... rather than erroneous execution
> >
> >No, you have it all wrong ...there....  Not raise an exception, but rather
> >gracefully take the end-of-walk branch of code, just as in normal 
> >operations.
> 
> Walking is only a small portion of the usage of cursors, and IMHO it is the 
> least important one (since everyone other than container developers ought to 
> be using iterators to walk their containers).
> 
> A cursor is a handle accessing an element of a larger container, nothing 
> more or less than that. The primary usage is to connect data structures made 
> up of multiple containers. For instance, consider a compiler symboltable. 
> There is a tree structure that represents each of the declarations and their 
> scopes, and a map structure that represents a mapping of names to nodes of 
> the treee. The contents of that map is going to be tree cursors, each 
> representing a declaration with a particular name.
> 
> In such a structure, it would be common to assume that the cursors are valid 
> (just like you would assume that pointers are non-null in such a case --  
> that's precisely what Janus/Ada code does, for instance). And dereferencing 
> a cursor that points at a deleted node has to raise some exception (just as 
> it would when using a pointer).
> 
> The value of cursors is that they can be implemented by a range of 
> abstractions with a range of checking, from array indicies (as in the 
> bounded containers and the vector) to pointers with a variety of schemes 
> from no dangling checking to the bulletproof controlled cursor scheme.

Interesting (ab)use case for cursors:  (ab)use cursors as an obfuscated long-lived address/pointer/access instead of for transiently walking  the contents of containers.  (The walk might be of only one or few results of a transient query, but still a walk of the transient results of the search.)  What you describe as (a[n ab]use case for) cursors is in reality a pointer in the end, despite any slight-of-hand to change what noun-phrase is utilized to name what in the end is quite clearly still a pointer(-in-purpose-&-mission).  A rose by any other name is just as pungent.

To put it SQL terms to reveal how jarring the (ab)use-case of cursors is, should a cursor be able to be stored as a field or record in a table?  The SQL answer is:  of course not, cursors are transient artifacts of dynamic queries, not able to be ossified in static storage.

My words are not a harsh critique or condemnation of Ada or of anyone's programming style; you are playing the cards that you are dealt.  It is food for my contemplation of this interim era of programming that lacks BetterAda or BetterRust as available programming languages.  (I'd say BetterC++, but that would be like saying BetterAbjectPoverty, where adding any richness makes poverty or C++ not poverty or C++ anymore.)  Today's Ada is closer to BetterAda than any other language is.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-20  1:28                               ` Jere
@ 2019-03-20  8:42                                 ` Dmitry A. Kazakov
  2019-03-22  2:00                                 ` Randy Brukardt
  1 sibling, 0 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-20  8:42 UTC (permalink / raw)


On 2019-03-20 02:28, Jere wrote:
> On Tuesday, March 19, 2019 at 7:13:47 PM UTC-4, Randy Brukardt wrote:
>>
>> Sadly, what I see here is someone who's so bought into Rust hype that they
>> fail to consider the real trade-offs implicit in such a technology. There's
>> no reason to bring the basic Rust scheme into Ada, since there is almost no
>> reason in Ada to create such pointers in the first place (see my reply to
>> Paul).
> 
> I'd say the biggest area that forces me to use access types is when
> dealing with complex limited types.

True. All boils down old issues:

1. Language-controlled references to access insides of containers.

2. Array abstraction to iterate using loops and #1 instead of 
pointer/handle/iterator.

3. Proper construction, especially for limited types, in order to 
initialize in-place using parameters. Limited return will never fly.

> If I want to use any kind of container
> implementation for a collection of limited types, I am forced to roll
> my own and generally have to use access types somewhere.  Same if I need
> to use a limited type in non limited context.

There is a difference between using pointers in order to implement 
something you could not do without them and reference semantics. 
Aliasing is an undesired effect in the former case and a requirement in 
the latter.

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-20  1:28                               ` Jere
  2019-03-20  8:42                                 ` Dmitry A. Kazakov
@ 2019-03-22  2:00                                 ` Randy Brukardt
  2019-03-22 11:10                                   ` Jere
  1 sibling, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-22  2:00 UTC (permalink / raw)


"Jere" <jhb.chat@gmail.com> wrote in message 
news:94a74b21-9c35-4f90-90f8-6262cde49e20@googlegroups.com...
...
> You would think that a container of limited types would be very 
> restrictive,
> but with the advent of Implicit_Dereference and reference types, there
> is definitely some meat there.  I would say maps and lists are the two
> areas I find the most need.

A container of a limited type would be very restrictive. ;-)

Several of us (including me) have tried to imagine how a container of 
limited objects would work, but it just doesn't make much sense. The primary 
problem is that one cannot control the lifetime of objects in a container, 
which includes the problem that one can't control the initialization of 
objects in a container. Whereas for non-limited objects, one just replaces 
them with the right data, you can't do that for a limited object. And since 
the initialization needs are type-dependent, there's no good way to deal 
with it in a type-safe manner. (A constructor with an unknown set of 
parameters isn't going to be type-safe, and with any particular set of 
parameters is too limiting.

Note that the same sort of thing applies to controlled objects -- it's not 
recommended to put controlled objects into any of the Ada.Containers with 
the possible exception of the undefinite containers. That's because the 
creation and destruction of objects is up to the container, not under any 
sort of program control. (Deleting an element does not necessarily delete 
the object.)

                             Randy.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-20  7:59                               ` Optikos
@ 2019-03-22  2:16                                 ` Randy Brukardt
  2019-03-22  8:38                                   ` Optikos
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-22  2:16 UTC (permalink / raw)


"Optikos" <optikos@verizon.net> wrote in message 
news:74339f3f-9591-45a3-8632-8834b4b466ab@googlegroups.com...
...
>What you describe as (a[n ab]use case for) cursors is in reality
>a pointer in the end, ...

Not a pointer, since a pointer is essentially a raw machine address which 
cannot detect problems. I'd call it a reference, as the abstract way of 
designating something.

And cursors can be and often are implemented so that the likelihood of an 
undetected dangling reference is low to impossible. That's not possible for 
any sort of pointer. (You can do the Rust thing and do some sort of 
compile-time rules, but that doesn't help build complex data structures.)

I don't believe that it is possible to build a complex data structure like 
an Ada compiler without some form of references. One can argue about the 
form, but not the need. You have to be able to have long-lived connections 
between structures -- they could be strong or weak or a variety of other 
things, but you can't live without some form of references.

                            Randy.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-20  1:08                             ` Jere
@ 2019-03-22  2:26                               ` Randy Brukardt
  2019-03-23 15:56                                 ` Jeffrey R. Carter
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-22  2:26 UTC (permalink / raw)


"Jere" <jhb.chat@gmail.com> wrote in message 
news:5dbd0a83-2d28-4c39-a973-2f0365d93846@googlegroups.com...
> On Tuesday, March 19, 2019 at 6:26:51 PM UTC-4, Paul Rubin wrote:
>> "Randy Brukardt" writes:
>> > Rust...  You can't build a cursor that way (nor a doubly-linked
>> > list). Perhaps the Rust people have gone beyond simple borrow
>> > semantics -- I don't know.
>>
>> I did a little web searching and it does seem to me that as of a year or
>> so ago, the way to make doubly linked lists in Rust was to call some
>> kind of unchecked library.  I'd like to know how it's done in ATS, and
>> I might ask on a Rust chat if it's still like that in Rust.
>>
>> I think it might be a serious issue for Rust, since one of Rust's
>> driving applications was web browsers.  Those build DOM trees where
>> nodes point to both their children and their parent, so the tree is full
>> of cycles.
>
> If you need either doubly linked lists or maps in Rust, you use the
> ones provided by the standard library (std::collections::list, for
> example, is the doubly linked list).  It's not unchecked at all.

But then why do you need pointers at all? The only cases where they are 
interesting is when they are heavily aliased; otherwise, you're better off 
using containers from the standard library or even your own types (as in Ada 
discriminated records). And it's that sort of aliasing that Rust is aiming 
to eliminate.

I'm sure that there is *some* example (there always is some example :-), but 
hardly enough to make something a programming language feature.

What I'm concerned about primarily is the ability to build ADTs that work 
like the Ada containers. If you have to do a bunch of unchecked stuff to do 
that, then they aren't safe at all. And one can't expect the 
implementation's library to provide *everything* for you.

                                                      Randy.





^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-20  1:20                           ` Jere
@ 2019-03-22  2:30                             ` Randy Brukardt
  2019-03-22  9:08                               ` Dmitry A. Kazakov
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-22  2:30 UTC (permalink / raw)


"Jere" <jhb.chat@gmail.com> wrote in message 
news:f610da94-1309-4cb6-8c7b-47f3099381e5@googlegroups.com...
...
> I don't know if you saw my earlier question to you (from a while back in
> this email chain), but do you know if Tucker was looking at the recent
> upgrades to the ownership scheme?  Some of them may (or may not) be useful
> for Ada (if that gets implemented).  In particular, in the old ownership
> scheme, if you needed to use a throwaway variable to capture a return 
> result
> in Rust, you couldn't reborrow again until that throwaway variable went
> out of scope.  In the updated system, they are able to tell it is 
> throwaway
> and allow for the ownership transfer.  I was thinking about this for
> Ada particularly since we are required to capture function returns into
> some sort of variable.

I can't speak to what Tucker did or did not read about, but the latest 
approach uses a mix of compile-time and runtime checks to ensure that the 
owner really is the owner of the designated object. He has a number of 
examples using discriminants to carry the owner along at runtime (this is 
roughly how cursors already work in the Ada.Containers anyway, so it isn't a 
big change for them).

I'm pretty sure the SPARK people are only interested in static checks, for 
the obvious reason that they are only interested in static checks in 
general.

                      Randy.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22  2:16                                 ` Randy Brukardt
@ 2019-03-22  8:38                                   ` Optikos
  2019-03-22 10:54                                     ` Jere
  0 siblings, 1 reply; 146+ messages in thread
From: Optikos @ 2019-03-22  8:38 UTC (permalink / raw)


On Thursday, March 21, 2019 at 10:16:24 PM UTC-4, Randy Brukardt wrote:
> "Optikos" wrote in message 
> news:74339f3f-9591-45a3-8632-8834b4b466ab@googlegroups.com...
> ...
> >What you describe as (a[n ab]use case for) cursors is in reality
> >a pointer in the end, ...
> 
> Not a pointer, since a pointer is essentially a raw machine address which 
> cannot detect problems. I'd call it a reference, as the abstract way of 
> designating something.
> 
> And cursors can be and often are implemented so that the likelihood of an 
> undetected dangling reference is low to impossible. That's not possible for 
> any sort of pointer. (You can do the Rust thing and do some sort of 
> compile-time rules, but that doesn't help build complex data structures.)

I am suspecting the same failure there in Rust.

> I don't believe that it is possible to build a complex data structure like 
> an Ada compiler without some form of references. One can argue about the 
> form, but not the need. You have to be able to have long-lived connections 
> between structures -- they could be strong or weak or a variety of other 
> things, but you can't live without some form of references.

On that, we wholeheartedly agree.  I look at programming as with any other flow of human endeavor based on philosophy & politics (with emphasis on the root-word policy within politics & police).  Some ideas, philosophies, policies (and their surrounding politics & police), and designs can carry a civilization (or programming community) only so far.  Sometimes “so far” is measured in centuries.  Other times “so far” is measured in decades or even only years.  We now see that the PL/1 & Ada wise vision of the foundational 1970s (which C++ absconded with too) takes us this far, but perhaps not much further.

What might take us further is an intimate side-channel among containers to have inter-container long-lived referencing that is •not outside• either the referencED container nor the higher-order referencING container, but rather a private matter within/among the federated containers—and is thus an alternate form of the encapsulation of ownership of these long-lived references, so that they are not dangling outside the built-up federated containers, and their lifetimes are guaranteed to be retired as each element of the container-federation is retired.  (Rust in particular seems to be incapable of expressing such federation to its current borrow checker.)  This seems to need some form of multistage programming which is to place at least:
1) [to borrow the #PL/1 & a.app Ada & OCaml P4 concept] an interpreter in the compiler to touch up the extrapolation of the encapsulation of the references in the federated containers
or
2) something more in the logic(-declaration-of-requirements) domain akin to Z (Zed) or ATS/LF to specify through stepwise refinement how the federation is to behave with respect to the encapsulation of the interplay of references among federated containers.

Then there can be stricter police (e.g., Rust's borrow checker; Tucker's first proposal) that assures no dangling pointers outside of what has been encapsulated within the overt declarations of how the federated containers reference each other.  What Rust has now is what perhaps history might call a naïve borrow checker that cannot be steered (at time of app-domain language-usage) by (app-domain-)federated containers.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22  2:30                             ` Randy Brukardt
@ 2019-03-22  9:08                               ` Dmitry A. Kazakov
  2019-03-22 22:23                                 ` Optikos
  0 siblings, 1 reply; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-22  9:08 UTC (permalink / raw)


On 2019-03-22 03:30, Randy Brukardt wrote:

> I'm pretty sure the SPARK people are only interested in static checks, for
> the obvious reason that they are only interested in static checks in
> general.

Not only SPARK people. From practical point of view any dynamic check is 
a lingering disaster, added complexity and, in general, a lie.

With dynamic checks you write code as if there were no branches in it, 
ignoring the fact that the code branches at all places where the check 
occurs.

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


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22  8:38                                   ` Optikos
@ 2019-03-22 10:54                                     ` Jere
  2019-03-23  7:53                                       ` Randy Brukardt
  0 siblings, 1 reply; 146+ messages in thread
From: Jere @ 2019-03-22 10:54 UTC (permalink / raw)


On Friday, March 22, 2019 at 4:38:29 AM UTC-4, Optikos wrote:
> On Thursday, March 21, 2019 at 10:16:24 PM UTC-4, Randy Brukardt wrote:
> > "Optikos" wrote in message 
> > ...
> > >What you describe as (a[n ab]use case for) cursors is in reality
> > >a pointer in the end, ...
> > 
> > Not a pointer, since a pointer is essentially a raw machine address which 
> > cannot detect problems. I'd call it a reference, as the abstract way of 
> > designating something.
> > 
> > And cursors can be and often are implemented so that the likelihood of an 
> > undetected dangling reference is low to impossible. That's not possible for 
> > any sort of pointer. (You can do the Rust thing and do some sort of 
> > compile-time rules, but that doesn't help build complex data structures.)
> 
> I am suspecting the same failure there in Rust.
> 

Not really.  In Rust they don't even use cursors.  They go straight to
iterators.  On top of that, the combination of being able to specify the 
lifetime of all of your variables (if you need to) and the ownership rules 
gives them 100% safety from dangling references when they create and use
those iterators.  

I can't speak for all of Ada, but it looks like GNAT starts with the 
assumption that the internal access type is valid (verifies not null), 
de-references it, and starts checking various elements of the de-referenced 
element/container (things like Next and Previous links when they exist, 
or Parent if it exists).  I think it even traverses a few nodes down 
whatever data structure they happen to be using for good measure.  
It's a good sequence of checks, but not full proof.  You could,
theoretically (but very unlikely) have de-referenced random memory that
just happened to look correct.  I don't know how other compilers do it
though.  

I don't think (or mean to imply) that Ada can't do equivalent or better
to Rust.  I am just saying, the couple of versions of GNAT I currently 
have do no yet.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-08 16:43 Olivier Henley
                   ` (3 preceding siblings ...)
  2019-03-13 13:23 ` Olivier Henley
@ 2019-03-22 11:10 ` Lucretia
  2019-03-22 14:09   ` J-P. Rosen
  2019-03-22 16:41   ` Jeffrey R. Carter
  2019-04-01  7:28 ` gautier_niouzes
  5 siblings, 2 replies; 146+ messages in thread
From: Lucretia @ 2019-03-22 11:10 UTC (permalink / raw)


See in: https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/47

> He also told me that Ada compilers aren’t allowed to do certain kinds of optimizations that for example c, c++ (and Rust and other PL via LLVM) are doing.

How true is this?


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22  2:00                                 ` Randy Brukardt
@ 2019-03-22 11:10                                   ` Jere
  2019-03-23  8:03                                     ` Randy Brukardt
  0 siblings, 1 reply; 146+ messages in thread
From: Jere @ 2019-03-22 11:10 UTC (permalink / raw)


On Thursday, March 21, 2019 at 10:00:41 PM UTC-4, Randy Brukardt wrote:
> "Jere" wrote in message 
> ...
> > You would think that a container of limited types would be very 
> > restrictive,
> > but with the advent of Implicit_Dereference and reference types, there
> > is definitely some meat there.  I would say maps and lists are the two
> > areas I find the most need.
> 
> A container of a limited type would be very restrictive. ;-)
> 
> Several of us (including me) have tried to imagine how a container of 
> limited objects would work, but it just doesn't make much sense. The primary 
> problem is that one cannot control the lifetime of objects in a container, 
> which includes the problem that one can't control the initialization of 
> objects in a container. Whereas for non-limited objects, one just replaces 
> them with the right data, you can't do that for a limited object. And since 
> the initialization needs are type-dependent, there's no good way to deal 
> with it in a type-safe manner. (A constructor with an unknown set of 
> parameters isn't going to be type-safe, and with any particular set of 
> parameters is too limiting.
> 

Yes constructors pose a problem.  The way I work around it is similar to
how Generic_Dispatching_Constructors does.  I let them define a parameter
which could be a record of parameters.

That said, it usually doesn't matter for limited types. When I have had to
make and use containers of limited types, I am in one of two places:

1.  The limited type was only made limited because of a component or two
so the designer created a copy procedure.  This lets me mostly treat
limited types the same as non limited types.  I've literally taken a GNAT
container, added a copy procedure formal to the generic, and integrated
it into the business logic whereever the compiler told me it couldn't 
copy a limited type.  So far that has worked flawlessly, but I don't
know if the customer has tried all of the various functions in the
containers.  This is the less likely case however.

2.  I don't worry about integrating initialization.  I just have the
container create a default object, and then I can use the combination
of cursors and references (or simply a "for of" loop) and initialize
them after adding them.  So yes, definitely more restrictive than
a non limited type container.  I just meant the restrictions were
not as insurmountable as I have seen in discussions before.  This
is the more often case.  This doesn't 100% cover all remaining cases
(like ones where you have to initialize the object at creation), 
but it has been the remaining 95% solution and very effective.  In
one case I created a package with the same operations as the customer's
but implemented the logic as an Ordered_Map of limited types instead
of the array logic they were using, and it increased their through
put by 3x (they did a lot of manual searching).  It also happened
to get a couple of their own programmers to rethink on how they
perceived Ada to be an "old" language (very pervasive thought 
where I work).  They had no idea that you could even make iterators
in Ada.  A couple didn't even know you could do dynamic dispatching 
as they started in Ada83 and never grew past that.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22 11:10 ` Lucretia
@ 2019-03-22 14:09   ` J-P. Rosen
  2019-03-22 16:41   ` Jeffrey R. Carter
  1 sibling, 0 replies; 146+ messages in thread
From: J-P. Rosen @ 2019-03-22 14:09 UTC (permalink / raw)


Le 22/03/2019 à 12:10, Lucretia a écrit :
> See in: https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/47
> 
>> He also told me that Ada compilers aren’t allowed to do certain kinds of optimizations that for example c, c++ (and Rust and other PL via LLVM) are doing.
> 
> How true is this?
> 
In Ada, the principle is that the compiler  has an obligation of result, 
i.e. that the "external effect" (see 1.1.3(9)) of the compiled program 
must be the same as the effect defined by the canonical execution.

Basically, this means that the compiler can do any optimization provided 
the result is correct. Going farther than that would mean allowing the 
compiler to generate incorrect programs... Maybe that's what C/C++ 
compilers are doing ;-)

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22 11:10 ` Lucretia
  2019-03-22 14:09   ` J-P. Rosen
@ 2019-03-22 16:41   ` Jeffrey R. Carter
  2019-03-22 17:29     ` Paul Rubin
  1 sibling, 1 reply; 146+ messages in thread
From: Jeffrey R. Carter @ 2019-03-22 16:41 UTC (permalink / raw)


On 3/22/19 12:10 PM, Lucretia wrote:
> See in: https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/47
> 
>> He also told me that Ada compilers aren’t allowed to do certain kinds of optimizations that for example c, c++ (and Rust and other PL via LLVM) are doing.
> 
> How true is this?

In the late 1980s-early 1990s there was a company named Tartan that sold C 
compilers for TI chips. TI chips came with a free C compiler, but people were 
willing to pay for the Tartan compilers because of their excellent optimization.

Tartan also sold Ada compilers with excellent optimization (see the "Ada 
Outperforms Assembly" paper). There were some papers published (probably in /Ada 
Letters/) in which the compiler writers demonstrated that their Ada compilers 
were faster than their C compilers, and discussed reasons why. One reason I 
recall was that in Ada, the compiler knew what was aliased and what wasn't, 
while in C everything is implicitly aliased, and this allowed optimizations of 
Ada that could not be done for C.

So for Ada 83 circa 1990, this statement is clearly false. With another 30 years 
of optimization technology behind us, I don't know for sure, but I suspect that 
hasn't changed.

-- 
Jeff Carter
"Crucifixion's a doddle."
Monty Python's Life of Brian
82

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22 16:41   ` Jeffrey R. Carter
@ 2019-03-22 17:29     ` Paul Rubin
  2019-03-22 22:36       ` Optikos
  0 siblings, 1 reply; 146+ messages in thread
From: Paul Rubin @ 2019-03-22 17:29 UTC (permalink / raw)


"Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> writes:
> In the late 1980s-early 1990s... in Ada, the compiler knew what was
> aliased and what wasn't, while in C everything is implicitly aliased,
> and this allowed optimizations of Ada that could not be done for C.

C later got the "restrict" keyword to help deal with this.  Also by the
late 1980s ANSI C was standardized saying that objects of differing
types couldn't be aliased, or the notorious UB would result.  That
probably made some uses of pointer casting illegal, that may have been
common in programs back then.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22  9:08                               ` Dmitry A. Kazakov
@ 2019-03-22 22:23                                 ` Optikos
  2019-03-27 19:20                                   ` G. B.
  0 siblings, 1 reply; 146+ messages in thread
From: Optikos @ 2019-03-22 22:23 UTC (permalink / raw)


On Friday, March 22, 2019 at 5:08:49 AM UTC-4, Dmitry A. Kazakov wrote:
> On 2019-03-22 03:30, Randy Brukardt wrote:
> 
> > I'm pretty sure the SPARK people are only interested in static checks, for
> > the obvious reason that they are only interested in static checks in
> > general.
> 
> Not only SPARK people. From practical point of view any dynamic check is 
> a lingering disaster, added complexity and, in general, a lie.
> 
> With dynamic checks you write code as if there were no branches in it, 
> ignoring the fact that the code branches at all places where the check 
> occurs.

Although Dmitry & I don't often agree, this time he speaks wisdom & truth.  The mathematical proof of no-leak, no-incorrect-pointer-arithmetic pointer-correctness must be 100% static (at compile-time) to be useful.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22 17:29     ` Paul Rubin
@ 2019-03-22 22:36       ` Optikos
  0 siblings, 0 replies; 146+ messages in thread
From: Optikos @ 2019-03-22 22:36 UTC (permalink / raw)


On Friday, March 22, 2019 at 1:29:53 PM UTC-4, Paul Rubin wrote:
> "Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> writes:
> > In the late 1980s-early 1990s... in Ada, the compiler knew what was
> > aliased and what wasn't, while in C everything is implicitly aliased,
> > and this allowed optimizations of Ada that could not be done for C.
> 
> C later got the "restrict" keyword to help deal with this.

  But is the restrict keyword actually utilized in industrial practice outside of benchmarks and perhaps high-performance numerical processing?  (I thought that the HPC people were all migrating to Julia as the new darling, btw.)

> Also by the
> late 1980s ANSI C was standardized saying that objects of differing
> types couldn't be aliased, or the notorious UB would result.  That
> probably made some uses of pointer casting illegal, that may have been
> common in programs back then.

By Jeffrey Carter's mentioning of early 1990s, K&R C had died a quick death in industrial practice by the early 1990s—mainly because industrial practice was utilizing C compilers •other than• AT&T issue3, issue4, or issue5 authentic reference-implementation compilers, so everyone was utilizing poor knock-offs of AT&T-issue K&R C.  Nearly every programmer and manager wanted to throw K&R C in the trashcan ASAP to flee from the compiler bugs & odd features/hacks that ANSI C corrected (ANSI C 1988's & ISO C 1990's trigraph & digraph abominations notwithstanding).

Conversely, in the early 1990s nearly 100% Ada83 compilers were from companies other than the authors of GNAT.  NYU's/Dewar's/Schonberg's EduAda83 was still an interpreter back then (and had no association with FSF GCC yet), so there was little interest in EduAda83 outside of university classrooms.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22 10:54                                     ` Jere
@ 2019-03-23  7:53                                       ` Randy Brukardt
  2019-03-23 13:59                                         ` Jere
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-23  7:53 UTC (permalink / raw)


"Jere" <jhb.chat@gmail.com> wrote in message 
news:5be8a4cc-84de-4716-9f0c-10907f451312@googlegroups.com...
...
> Not really.  In Rust they don't even use cursors.  They go straight to
> iterators.  On top of that, the combination of being able to specify the
> lifetime of all of your variables (if you need to) and the ownership rules
> gives them 100% safety from dangling references when they create and use
> those iterators.

If you don't store any cursors and just use iterators in Ada, you have the 
same level of safety: the tampering checks prevent any problems with 
iterators. (Well, unless you turn them off, of course, but if you remove the 
seatbelts, you can't much complain that they didn't protect you.)

I'd be interested to find out how Rust deals with the need to designate 
individual elements of a container (which is the primary reason that Ada 
exposes cursors).

                       Randy.




^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22 11:10                                   ` Jere
@ 2019-03-23  8:03                                     ` Randy Brukardt
  2019-03-23 21:32                                       ` Jere
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-23  8:03 UTC (permalink / raw)


The classic (and rare) example of a limited type is one containing a task. 
For those, you do need to control initialization. You also need to do so if 
the type has any discriminants.

I suppose it would be possible to do in a sense by defining *exactly* what 
every operation must do (essentially by providing the body) -- but then 
there is no reason to standardize it, because there is no value to be added 
by an implementer. (Anyone can download a library from github or whatever 
and compile with with whatever compiler you want.)

This is the same sort of reason it doesn't make much sense to allow 
user-defined storage pools in a container -- you would have to precisely 
define what allocators are going to do (in terms of allocation sizes, 
ordering,  and the like) so that a pool could take advantage of that. But 
then there's really nothing for the implementation to do - the package is so 
heavily specified that there is no freedom to improve the implementation.

                   Randy.

"Jere" <jhb.chat@gmail.com> wrote in message 
news:0e27ab0a-5daa-45b0-ae5c-a2441fb1ad40@googlegroups.com...
> On Thursday, March 21, 2019 at 10:00:41 PM UTC-4, Randy Brukardt wrote:
>> "Jere" wrote in message
>> ...
>> > You would think that a container of limited types would be very
>> > restrictive,
>> > but with the advent of Implicit_Dereference and reference types, there
>> > is definitely some meat there.  I would say maps and lists are the two
>> > areas I find the most need.
>>
>> A container of a limited type would be very restrictive. ;-)
>>
>> Several of us (including me) have tried to imagine how a container of
>> limited objects would work, but it just doesn't make much sense. The 
>> primary
>> problem is that one cannot control the lifetime of objects in a 
>> container,
>> which includes the problem that one can't control the initialization of
>> objects in a container. Whereas for non-limited objects, one just 
>> replaces
>> them with the right data, you can't do that for a limited object. And 
>> since
>> the initialization needs are type-dependent, there's no good way to deal
>> with it in a type-safe manner. (A constructor with an unknown set of
>> parameters isn't going to be type-safe, and with any particular set of
>> parameters is too limiting.
>>
>
> Yes constructors pose a problem.  The way I work around it is similar to
> how Generic_Dispatching_Constructors does.  I let them define a parameter
> which could be a record of parameters.
>
> That said, it usually doesn't matter for limited types. When I have had to
> make and use containers of limited types, I am in one of two places:
>
> 1.  The limited type was only made limited because of a component or two
> so the designer created a copy procedure.  This lets me mostly treat
> limited types the same as non limited types.  I've literally taken a GNAT
> container, added a copy procedure formal to the generic, and integrated
> it into the business logic whereever the compiler told me it couldn't
> copy a limited type.  So far that has worked flawlessly, but I don't
> know if the customer has tried all of the various functions in the
> containers.  This is the less likely case however.
>
> 2.  I don't worry about integrating initialization.  I just have the
> container create a default object, and then I can use the combination
> of cursors and references (or simply a "for of" loop) and initialize
> them after adding them.  So yes, definitely more restrictive than
> a non limited type container.  I just meant the restrictions were
> not as insurmountable as I have seen in discussions before.  This
> is the more often case.  This doesn't 100% cover all remaining cases
> (like ones where you have to initialize the object at creation),
> but it has been the remaining 95% solution and very effective.  In
> one case I created a package with the same operations as the customer's
> but implemented the logic as an Ordered_Map of limited types instead
> of the array logic they were using, and it increased their through
> put by 3x (they did a lot of manual searching).  It also happened
> to get a couple of their own programmers to rethink on how they
> perceived Ada to be an "old" language (very pervasive thought
> where I work).  They had no idea that you could even make iterators
> in Ada.  A couple didn't even know you could do dynamic dispatching
> as they started in Ada83 and never grew past that. 



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-23  7:53                                       ` Randy Brukardt
@ 2019-03-23 13:59                                         ` Jere
  2019-03-23 21:19                                           ` Jere
  2019-03-26  8:09                                           ` Optikos
  0 siblings, 2 replies; 146+ messages in thread
From: Jere @ 2019-03-23 13:59 UTC (permalink / raw)


On Saturday, March 23, 2019 at 3:53:34 AM UTC-4, Randy Brukardt wrote:
> "Jere" wrote in message 
> ...
> > Not really.  In Rust they don't even use cursors.  They go straight to
> > iterators.  On top of that, the combination of being able to specify the
> > lifetime of all of your variables (if you need to) and the ownership rules
> > gives them 100% safety from dangling references when they create and use
> > those iterators.
> 
> If you don't store any cursors and just use iterators in Ada, you have the 
> same level of safety: the tampering checks prevent any problems with 
> iterators. (Well, unless you turn them off, of course, but if you remove the 
> seatbelts, you can't much complain that they didn't protect you.)
> 
> I'd be interested to find out how Rust deals with the need to designate 
> individual elements of a container (which is the primary reason that Ada 
> exposes cursors).
> 
>                        Randy.

Keep in mind the rust paradigm is very different than Ada's.  When you
obtain an iterator of a container, you borrow ownership of the container.
At that point it is impossible to tamper with the container because it
is a compile time error to modify the container when something else has 
ownership of it. It's a compile time version of Ada's tampering checks
using an ownership model.  If you need to remove items as you iterate, 
there is a consuming version of the iterator that allows for that. It
handles all the logic of keeping the iterator correct as you remove
items.  If you need to remove only specific items, it provides 
functions for that as well (but you would not iterate while using 
them do to the ownership/borrowing rules).

Additionally, Rust allows you to specify the lifetime of the iterator, 
the lifetime of the reference to the item, and how they relate to the
lifetime of the container so that the compiler can guarantee that
nothing dangles (it's a relative specification..container has lifetime 
A and everything else has either A or a lifetime relative to A).

If you were instead referring to indexing the container, for things
like vector, Rust looks to see if the container implements the Index
trait, and, if so, allows for the user to use the index operation
on the container.  It's very similar to making a cursor and setting the
variable_indexing aspect and constant_indexing aspect, except rust doesn't
expose the underlying equivalent cursor type.  So you either work
with Indexes or Iterators depending on your need.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22  2:26                               ` Randy Brukardt
@ 2019-03-23 15:56                                 ` Jeffrey R. Carter
  2019-03-23 21:38                                   ` Paul Rubin
  0 siblings, 1 reply; 146+ messages in thread
From: Jeffrey R. Carter @ 2019-03-23 15:56 UTC (permalink / raw)


On 3/22/19 3:26 AM, Randy Brukardt wrote:
> 
> But then why do you need pointers [in Rust] at all? The only cases where they are
> interesting is when they are heavily aliased; otherwise, you're better off
> using containers from the standard library or even your own types (as in Ada
> discriminated records). And it's that sort of aliasing that Rust is aiming
> to eliminate.

 From what I've read about Rust, it's a fairly typical C-family language, except 
for the borrow rules. Pointers (by whatever name and with whatever restrictions) 
are pervasive. One must explicitly pass a pointer to avoid pass-by-copy for 
large objects, or to obtain [in] out semantics. Every example of Rust I've seen 
has been filled with the various symbols for pointers.

-- 
Jeff Carter
"They name the boy Jonathan Ralph Starkwell,
after Virgil's mother."
Take the Money and Run
141


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-23 13:59                                         ` Jere
@ 2019-03-23 21:19                                           ` Jere
  2019-03-23 21:29                                             ` Paul Rubin
  2019-03-26  8:09                                           ` Optikos
  1 sibling, 1 reply; 146+ messages in thread
From: Jere @ 2019-03-23 21:19 UTC (permalink / raw)


On Saturday, March 23, 2019 at 9:59:38 AM UTC-4, Jere wrote:
> On Saturday, March 23, 2019 at 3:53:34 AM UTC-4, Randy Brukardt wrote:
> > "Jere" wrote in message 
> > ...
> > > Not really.  In Rust they don't even use cursors.  They go straight to
> > > iterators.  On top of that, the combination of being able to specify the
> > > lifetime of all of your variables (if you need to) and the ownership rules
> > > gives them 100% safety from dangling references when they create and use
> > > those iterators.
> > 
> > If you don't store any cursors and just use iterators in Ada, you have the 
> > same level of safety: the tampering checks prevent any problems with 
> > iterators. (Well, unless you turn them off, of course, but if you remove the 
> > seatbelts, you can't much complain that they didn't protect you.)
> > 
> > I'd be interested to find out how Rust deals with the need to designate 
> > individual elements of a container (which is the primary reason that Ada 
> > exposes cursors).
> > 
> >                        Randy.
> 
> Keep in mind the rust paradigm is very different than Ada's.  

Randy (and others), I realized I have said a lot about Rust in this
discussion.  I don't want overshadow the fact that I think Ada
is the superior language.  I've just done some programming in Rust, 
so I felt I could give some insight on the different aspects. I 
apologize if I am saying too much on the topic.  I do feel there 
are things that Ada can learn from Rust, but that doesn't mean
I think Rust is overall better. 


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-23 21:19                                           ` Jere
@ 2019-03-23 21:29                                             ` Paul Rubin
  0 siblings, 0 replies; 146+ messages in thread
From: Paul Rubin @ 2019-03-23 21:29 UTC (permalink / raw)


Jere <jhb.chat@gmail.com> writes:
> Randy (and others), I realized I have said a lot about Rust in this
> discussion.  I don't want overshadow the fact that I think Ada
> is the superior language.  I've just done some programming in Rust, 
> so I felt I could give some insight on the different aspects.

Please continue, I like seeing the comparisons.  

> I do feel there are things that Ada can learn from Rust, but that
> doesn't mean I think Rust is overall better.

I don't have a view on "overall better", but it seems to me that each
one has particular areas of being better, so they can learn from each
other.  Therefore, detailed comparisons are a good thing.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-23  8:03                                     ` Randy Brukardt
@ 2019-03-23 21:32                                       ` Jere
  0 siblings, 0 replies; 146+ messages in thread
From: Jere @ 2019-03-23 21:32 UTC (permalink / raw)


On Saturday, March 23, 2019 at 4:03:15 AM UTC-4, Randy Brukardt wrote:
> The classic (and rare) example of a limited type is one containing a task. 
> For those, you do need to control initialization. You also need to do so if 
> the type has any discriminants.
> 
> I suppose it would be possible to do in a sense by defining *exactly* what 
> every operation must do (essentially by providing the body) -- but then 
> there is no reason to standardize it, because there is no value to be added 
> by an implementer. (Anyone can download a library from github or whatever 
> and compile with with whatever compiler you want.)
> 
> This is the same sort of reason it doesn't make much sense to allow 
> user-defined storage pools in a container -- you would have to precisely 
> define what allocators are going to do (in terms of allocation sizes, 
> ordering,  and the like) so that a pool could take advantage of that. But 
> then there's really nothing for the implementation to do - the package is so 
> heavily specified that there is no freedom to improve the implementation.
> 
>                    Randy.
> 
I really just wish that Ada would find a way to close those remaining
holes.  I've had the discussion before with others about access types,
but it is hard to make the argument to others that in Ada you don't
have to use Access types, when the reality is that is only mostly true.
I would like to get to a point where the only time I need to use
unchecked_deallocation in my own code, is when I have to do something
for performance reasons.  Even if that is simply some sort of smart 
access wrappers provided by the standard that work for limited types.
I feel like something as basic as memory deallocation should have more
automatic coverage options in the language.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-23 15:56                                 ` Jeffrey R. Carter
@ 2019-03-23 21:38                                   ` Paul Rubin
  0 siblings, 0 replies; 146+ messages in thread
From: Paul Rubin @ 2019-03-23 21:38 UTC (permalink / raw)


"Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> writes:
> From what I've read about Rust, it's a fairly typical C-family
> language, except for the borrow rules. Pointers (by whatever name and
> with whatever restrictions) are pervasive.

I haven't done any Rust yet, but "modern" C++ style avoids pointers and
uses references instead.  One can now (post C++11) write idiomatic C++
code with few if any pointers.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
@ 2019-03-25 19:14 Randy Brukardt
  2019-03-25 20:44 ` Dmitry A. Kazakov
  2019-03-28  0:48 ` Jere
  0 siblings, 2 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-03-25 19:14 UTC (permalink / raw)


"Jere" <jhb.chat@gmail.com> wrote in message
news:735761d5-f917-4477-9b0a-e0cde1ce2440@googlegroups.com...
> On Saturday, March 23, 2019 at 3:53:34 AM UTC-4, Randy Brukardt wrote:
...
> If you were instead referring to indexing the container, for things
> like vector, Rust looks to see if the container implements the Index
> trait, and, if so, allows for the user to use the index operation
> on the container.  It's very similar to making a cursor and setting the
> variable_indexing aspect and constant_indexing aspect, except rust doesn't
> expose the underlying equivalent cursor type.  So you either work
> with Indexes or Iterators depending on your need.

I was specifically asking about the common need to have connections between
containers. It's not likely that a single container is all one needs to
solve a problem, so one needs ways to refer to elements of one container
from another.

For instance, one might need a index for another container. (For instance,
to allow lookups by some internal characteristic.) If the main container is
structured (as in an internal representation of HTML or XML, or a compiler
symbol table), the index has to be a separate container. Ada provides
cursors to represent those sorts of interconnections. How does Rust do it??
(If it does it at all.)

This sort of thing comes up any time that one has two separate data
structures that are inter-related. Sometimes you can use composition for
combining structures (and that's preferable when possible), but if there are
potentially multiple references to a single item or if the element is just
part of a larger data structure, composition doesn't work and some sort of
reference is needed.

                       Randy.

P.S. Sorry about breaking the thread; the message wouldn't post because of 
header limits (too many replies).




^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-25 19:14 Intervention needed? Randy Brukardt
@ 2019-03-25 20:44 ` Dmitry A. Kazakov
  2019-03-28  0:48 ` Jere
  1 sibling, 0 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-25 20:44 UTC (permalink / raw)


On 2019-03-25 20:14, Randy Brukardt wrote:

> I was specifically asking about the common need to have connections between
> containers. It's not likely that a single container is all one needs to
> solve a problem, so one needs ways to refer to elements of one container
> from another.

Example: a relational table searchable by keys K1..KN containing data 
D1..DM. A typical implementation is a map Index->(D1,...,DM) and N maps 
Ki->Index.

> For instance, one might need a index for another container. (For instance,
> to allow lookups by some internal characteristic.) If the main container is
> structured (as in an internal representation of HTML or XML, or a compiler
> symbol table), the index has to be a separate container. Ada provides
> cursors to represent those sorts of interconnections.

Things become especially interesting with forward and backward 
references, transitive references and references marshaled from context 
to context.

> P.S. Sorry about breaking the thread; the message wouldn't post because of
> header limits (too many replies).

References again...

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-23 13:59                                         ` Jere
  2019-03-23 21:19                                           ` Jere
@ 2019-03-26  8:09                                           ` Optikos
  1 sibling, 0 replies; 146+ messages in thread
From: Optikos @ 2019-03-26  8:09 UTC (permalink / raw)


On Saturday, March 23, 2019 at 9:59:38 AM UTC-4, Jere wrote:
> On Saturday, March 23, 2019 at 3:53:34 AM UTC-4, Randy Brukardt wrote:
> > "Jere" wrote in message 
> > ...
> > > Not really.  In Rust they don't even use cursors.  They go straight to
> > > iterators.  On top of that, the combination of being able to specify the
> > > lifetime of all of your variables (if you need to) and the ownership rules
> > > gives them 100% safety from dangling references when they create and use
> > > those iterators.
> > 
> > If you don't store any cursors and just use iterators in Ada, you have the 
> > same level of safety: the tampering checks prevent any problems with 
> > iterators. (Well, unless you turn them off, of course, but if you remove the 
> > seatbelts, you can't much complain that they didn't protect you.)
> > 
> > I'd be interested to find out how Rust deals with the need to designate 
> > individual elements of a container (which is the primary reason that Ada 
> > exposes cursors).
> > 
> >                        Randy.
> 
> Keep in mind the rust paradigm is very different than Ada's.  When you
> obtain an iterator of a container, you borrow ownership of the container.
> At that point it is impossible to tamper with the container because it
> is a compile time error to modify the container when something else has 
> ownership of it. It's a compile time version of Ada's tampering checks
> using an ownership model.  If you need to remove items as you iterate, 
> there is a consuming version of the iterator that allows for that. It
> handles all the logic of keeping the iterator correct as you remove
> items.  If you need to remove only specific items, it provides 
> functions for that as well (but you would not iterate while using 
> them do to the ownership/borrowing rules).
> 
> Additionally, Rust allows you to specify the lifetime of the iterator, 
> the lifetime of the reference to the item, and how they relate to the
> lifetime of the container so that the compiler can guarantee that
> nothing dangles (it's a relative specification..container has lifetime 
> A and everything else has either A or a lifetime relative to A).

This overt specification of lifetime (vis a vis Ada's multiple fixed assumptions of lifetime) seems to be Rust's key innovative contribution that Ada lacks.  An analogous key contribution to humankind is that ATS2 and ATS3 base their guaranteed no-dangling-pointer correctness on “type* views” (and their type@address primitives in “viewtypes”) which are quite different syntactically than Rust's overt specification of lifetime but in the end provide to ATS a direct measure of extent of lifetime implied by (and directly derived from) what depending on what for how long.

* What ATS calls type is a branch of type-theory from higher mathematics.  What we call type in programming is generally called “sort” in ATS, where ATS's usage of sort has the meaning of “kind” or “category” as in ‘what sort of programmer are you?’, but ATS's usage of sort does not have the meaning of “order arrangement” as in the SQL-statement clause SORT.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-22 22:23                                 ` Optikos
@ 2019-03-27 19:20                                   ` G. B.
  2019-03-27 21:02                                     ` Paul Rubin
  0 siblings, 1 reply; 146+ messages in thread
From: G. B. @ 2019-03-27 19:20 UTC (permalink / raw)


Optikos <optikos@verizon.net> wrote:
> On Friday, March 22, 2019 at 5:08:49 AM UTC-4, Dmitry A. Kazakov wrote:
>> 
>> From practical point of view any dynamic check is 
>> a lingering disaster, added complexity and, in general, a lie.
>> 
>> With dynamic checks you write code as if there were no branches in it, 
>> ignoring the fact that the code branches at all places where the check 
>> occurs.

Something that perform checks is, I think, just proper management if there
is awareness of risk.

> The mathematical proof of no-leak, no-incorrect-pointer-arithmetic
> pointer-correctness must be 100% static (at compile-time) to be useful.
> 

For some N% of Ada programs, will a computation  of a proof be predictably
finished in time? 

Static knowledge is a privilege not shared by many, or much, I suppose.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-27 19:20                                   ` G. B.
@ 2019-03-27 21:02                                     ` Paul Rubin
  2019-03-28  7:01                                       ` Maciej Sobczak
  0 siblings, 1 reply; 146+ messages in thread
From: Paul Rubin @ 2019-03-27 21:02 UTC (permalink / raw)


G. B. <nonlegitur@nmhp.invalid> writes:
> For some N% of Ada programs, will a computation of a proof be
> predictably finished in time? .. Static knowledge is a privilege not
> shared by many, or much, I suppose.

If you haven't got some reasoning in your head that the program is
pointer-correct, you shouldn't deploy it.  If you do have some reasoning
that it is correct, the idea of a proof system is to let you write down
the reasoning in a way that it can be mechanically verified.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-25 19:14 Intervention needed? Randy Brukardt
  2019-03-25 20:44 ` Dmitry A. Kazakov
@ 2019-03-28  0:48 ` Jere
  1 sibling, 0 replies; 146+ messages in thread
From: Jere @ 2019-03-28  0:48 UTC (permalink / raw)


On Monday, March 25, 2019 at 3:14:38 PM UTC-4, Randy Brukardt wrote:
> "Jere" wrote in message
> > On Saturday, March 23, 2019 at 3:53:34 AM UTC-4, Randy Brukardt wrote:
> ...
> > If you were instead referring to indexing the container, for things
> > like vector, Rust looks to see if the container implements the Index
> > trait, and, if so, allows for the user to use the index operation
> > on the container.  It's very similar to making a cursor and setting the
> > variable_indexing aspect and constant_indexing aspect, except rust doesn't
> > expose the underlying equivalent cursor type.  So you either work
> > with Indexes or Iterators depending on your need.
> 
> I was specifically asking about the common need to have connections between
> containers. It's not likely that a single container is all one needs to
> solve a problem, so one needs ways to refer to elements of one container
> from another.
> 
> For instance, one might need a index for another container. (For instance,
> to allow lookups by some internal characteristic.) If the main container is
> structured (as in an internal representation of HTML or XML, or a compiler
> symbol table), the index has to be a separate container. Ada provides
> cursors to represent those sorts of interconnections. How does Rust do it??
> (If it does it at all.)
> 
> This sort of thing comes up any time that one has two separate data
> structures that are inter-related. Sometimes you can use composition for
> combining structures (and that's preferable when possible), but if there are
> potentially multiple references to a single item or if the element is just
> part of a larger data structure, composition doesn't work and some sort of
> reference is needed.
> 
>                        Randy.
> 
> P.S. Sorry about breaking the thread; the message wouldn't post because of 
> header limits (too many replies).

I generally don't come across situations that require this, so I don't know
how useful my answer will be.  Plus I've only programmed in Rust off and on
for fun on some side projects.  I mostly do either C or Ada as the platform
allows.

Generally, Rust looks at potential memory erroneous access as a 100% no
no, so the same method used in Ada with Cursors wouldn't be allowed.  They
have really really low chance, but there still is a chance.  From what
I could find on the topic, the general first suggestion is to rethink
your approach and pick a better solution that doesn't involve potentially
dangling references (similar to the mentality we often suggest to new
comers trying to port ideas from C/C++ into Ada directly without 
considering the Ada way).  

Aside from that, if you can't approach it very differently, there are
different options available.  For more temporary type situations (say
wanting to delete a subset of elements from a container), they provide
various map(), filter(), and collect() operations that interact with
the iterators to get the configuration you want.

For more long term containers (This sounds more like what you are asking
for), the methods I came across were to take a step back and determine
which of the 2 (or more) containers really needs to be the owner of the
data (it isn't always the one that common sense initially indicates), 
have it own the data using an owning reference, and have the other
containers use non-owning references (which you can promote to owning
references temporarily as needed).  That would be more along the lines
of the idiomatic "safe" approach.  This allows Rust to keep track
of who can use the reference when (using temporal rules) and doesn't 
involve any unsafe code.

That isn't a silver bullet for all situations though.  In some cases, 
you might have to use one standard container and another that you 
make from scratch and have the standard container integrate into the 
other one under the hood. 

I'm not a very seasoned Rust programmer, so I am probably missing some
other solutions.  I'm more comfortable in Ada and like to use it more
anyways.  I'm also sure you could come up with some situation where
the above suggestions wouldn't work.   I don't generally have a better
answer due to lack of experience.  And the answer may at some point
indeed involve unsafe programming. You are still required to maintain
the 100% memory safety, even in the case of using the "unsafe" keyword,
so something too similar to the Ada cursors method in its current form
would not be allowed.

Sorry for the long wait on the reply.  I wanted to do some test programming
to make sure the stuff I mentioned above would actually work and also
do some research on it since, in my problem domains, I don't ever run
into situations where container shadowing/interacting is required.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-27 21:02                                     ` Paul Rubin
@ 2019-03-28  7:01                                       ` Maciej Sobczak
  2019-03-28  7:17                                         ` Paul Rubin
  2019-03-28  9:06                                         ` Dmitry A. Kazakov
  0 siblings, 2 replies; 146+ messages in thread
From: Maciej Sobczak @ 2019-03-28  7:01 UTC (permalink / raw)


> > For some N% of Ada programs, will a computation of a proof be
> > predictably finished in time? .. Static knowledge is a privilege not
> > shared by many, or much, I suppose.
> 
> If you haven't got some reasoning in your head that the program is
> pointer-correct, you shouldn't deploy it.

This is an appealing perspective, but I agree that the privilege is not available in all situations (SPARK allows unchecked portions of code for a reason).

Which brings a potentially interesting question - what if the reasoning in my head has a continuous measure of correctness? Like, say, I'm 95% confident that the reasoning is correct? Should I deploy my system or not? The mechanical proof will fail 100% of the time, but that does not mean that the software is entirely useless for my user, who also has his own continuous measure of risk and level of failure acceptance.

The ability to work with continuous measures is what is practiced in every other engineering discipline (including critical ones!), yet the formal-method priests like you prevent me from deploying my acceptably correct programs. I find it a *limitation* of your methods, not mine.

Could you please fix your methods so that I can deploy my almost-certainly-correct system, like everybody else does, instead of forcing me to use tools that are demonstrably unfit for today's market needs? Thank you.

(disclaimer: playing the devil's advocate for a reason)

-- 
Maciej Sobczak * http://www.inspirel.com


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-28  7:01                                       ` Maciej Sobczak
@ 2019-03-28  7:17                                         ` Paul Rubin
  2019-03-28  8:39                                           ` Simon Wright
  2019-03-30 22:14                                           ` Robert A Duff
  2019-03-28  9:06                                         ` Dmitry A. Kazakov
  1 sibling, 2 replies; 146+ messages in thread
From: Paul Rubin @ 2019-03-28  7:17 UTC (permalink / raw)


Maciej Sobczak <see.my.homepage@gmail.com> writes:
> Which brings a potentially interesting question - what if the
> reasoning in my head has a continuous measure of correctness? Like,
> say, I'm 95% confident that the reasoning is correct? Should I deploy
> my system or not? The mechanical proof will fail 100% of the time, but
> that does not mean that the software is entirely useless for my user,
> who also has his own continuous measure of risk and level of failure
> acceptance.

I would say that in a high-assurance system (which is the normal
situation where one talks about SPARK and proofs), what you describe is
by definition not allowed.  That's using the notion of high-assurance
software from here:

https://dwheeler.com/essays/high-assurance-floss.html

Of course you could redefine your system to be medium-assurance and let
it through.  Usually that type of software is validated through more
conventional testing processes.

Fwiw, there's a video on Youtube of Adacore founder Bob Dewar talking
about the flight software for the F-22 fighter plane, where he asks
whether that software should be considered safety-critical.  The
audience laughs, but Dewar goes on to say that of course a passenger
plane's software is safety-critical, but the whole idea of a fighter
plane is to go up and get shot at, the controls let the pilot
deliberately run the engines above their power envelope, etc.  IIRC he
said that the F-22 program managers didn't buy that argument and still
wanted the software to be treated as safety-critical.

Be careful too of "normalization of deviance", the sociological process
that led the Space Shuttle staff to accept more and more misbehaviour
from the Shuttle until the Challenger exploded.  The term is from Diane
Vaughan's book "The Challenger Launch Decision", which I want to get
around to reading someday.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-28  7:17                                         ` Paul Rubin
@ 2019-03-28  8:39                                           ` Simon Wright
  2019-03-30  4:31                                             ` Paul Rubin
  2019-03-30 22:14                                           ` Robert A Duff
  1 sibling, 1 reply; 146+ messages in thread
From: Simon Wright @ 2019-03-28  8:39 UTC (permalink / raw)


Paul Rubin <no.email@nospam.invalid> writes:

> Fwiw, there's a video on Youtube of Adacore founder Bob Dewar talking
> about the flight software for the F-22 fighter plane, where he asks
> whether that software should be considered safety-critical.  The
> audience laughs, but Dewar goes on to say that of course a passenger
> plane's software is safety-critical, but the whole idea of a fighter
> plane is to go up and get shot at, the controls let the pilot
> deliberately run the engines above their power envelope, etc.  IIRC he
> said that the F-22 program managers didn't buy that argument and still
> wanted the software to be treated as safety-critical.

https://youtu.be/DnsLpEgFUSk I think. Only the slides, I think, but the
voice is distinctive!

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-28  7:01                                       ` Maciej Sobczak
  2019-03-28  7:17                                         ` Paul Rubin
@ 2019-03-28  9:06                                         ` Dmitry A. Kazakov
  2019-03-28 20:48                                           ` G. B.
  2019-03-29  6:57                                           ` Maciej Sobczak
  1 sibling, 2 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-28  9:06 UTC (permalink / raw)


On 2019-03-28 08:01, Maciej Sobczak wrote:

> Which brings a potentially interesting question - what if the reasoning in my head has a continuous measure of correctness? Like, say, I'm 95% confident that the reasoning is correct?

This is not how reasoning work. It is how the physical model does. 
Physical models have stochastic nature. The probabilistic measure is 
additive. But human reasoning is nowhere stochastic.

> Should I deploy my system or not? The mechanical proof will fail 100% of the time, but that does not mean that the software is entirely useless for my user, who also has his own continuous measure of risk and level of failure acceptance.

Nothing like that. You have states the physical system may go into with 
different probabilities. Some of these states are fail-states. It has 
nothing to do with proofs. If something is proven about a physical 
system, that would be a fact, not a statistical event. Fact /= event.

BTW, a digital system has an advantage that you can (theoretically) 
ensure some states never entered. You cannot do that with a physical 
system, there is always a non-zero probability that it would do nobody 
knows what.

> The ability to work with continuous measures is what is practiced in every other engineering discipline (including critical ones!), yet the formal-method priests like you prevent me from deploying my acceptably correct programs. I find it a *limitation* of your methods, not mine.

This again has nothing to do with measures, but with the Newtonian 
mechanics with limited masses and accelerations. The solutions there are 
smooth. Small changes of inputs produce small changes of outputs, except 
for few cases of chaotic systems etc.

These premises do not apply to digital systems. Programming languages 
like Ada are designed in a way to smooth the behavior a bit, in order to 
allow gradual design, but only a bit.

> Could you please fix your methods so that I can deploy my almost-certainly-correct system, like everybody else does, instead of forcing me to use tools that are demonstrably unfit for today's market needs? Thank you.

Very bad. This is a part of the problem as well. You cannot have it this 
way because old rules do not apply. Attempts to use quality assurance 
methods known in engineering disciplines to software result in 
nonsensical standards and certification procedures which assure nothing 
but wasting human resources.

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-28  9:06                                         ` Dmitry A. Kazakov
@ 2019-03-28 20:48                                           ` G. B.
  2019-03-29  5:13                                             ` Bojan Bozovic
  2019-03-29  6:57                                           ` Maciej Sobczak
  1 sibling, 1 reply; 146+ messages in thread
From: G. B. @ 2019-03-28 20:48 UTC (permalink / raw)


Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
> On 2019-03-28 08:01, Maciej Sobczak wrote:
> Attempts to use quality assurance 
> methods known in engineering disciplines to software result in 
> nonsensical standards and certification procedures which assure nothing 
> but wasting human resources.
> 

The equivalence class of economically viable software firms demonstrates
that there exist a sweet spot. It lies between investing in the production
of correct logic and selling software that has layers of waste.

For an analogy, compare compost and composites. 

Customers and programmers alike might say that anything with waste in it is
not sweet, it’s bitter. But, they are sheep. Enjoy Ada while you can.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-28 20:48                                           ` G. B.
@ 2019-03-29  5:13                                             ` Bojan Bozovic
  2019-03-29  8:13                                               ` Dmitry A. Kazakov
  0 siblings, 1 reply; 146+ messages in thread
From: Bojan Bozovic @ 2019-03-29  5:13 UTC (permalink / raw)


On Thursday, March 28, 2019 at 9:48:09 PM UTC+1, G. B. wrote:
> Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
> > On 2019-03-28 08:01, Maciej Sobczak wrote:
> > Attempts to use quality assurance 
> > methods known in engineering disciplines to software result in 
> > nonsensical standards and certification procedures which assure nothing 
> > but wasting human resources.
> > 
> 
> The equivalence class of economically viable software firms demonstrates
> that there exist a sweet spot. It lies between investing in the production
> of correct logic and selling software that has layers of waste.
> 
> For an analogy, compare compost and composites. 
> 
> Customers and programmers alike might say that anything with waste in it is
> not sweet, it’s bitter. But, they are sheep. Enjoy Ada while you can.

With Internet of Things and the like devices, self-driving cars etc. the need for correctness in software will only increase not otherwise. When computers can affect the environment physically matter of correct behaviour becomes paramount, so Ada really have the future. What's important is to promote it outside of safety-critical software, for general programming, so that those that don't even know about Ada now can learn it and use it.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-28  9:06                                         ` Dmitry A. Kazakov
  2019-03-28 20:48                                           ` G. B.
@ 2019-03-29  6:57                                           ` Maciej Sobczak
  2019-03-29  7:13                                             ` Paul Rubin
  2019-03-29  8:39                                             ` Dmitry A. Kazakov
  1 sibling, 2 replies; 146+ messages in thread
From: Maciej Sobczak @ 2019-03-29  6:57 UTC (permalink / raw)


> > Which brings a potentially interesting question - what if the reasoning in my head has a continuous measure of correctness? Like, say, I'm 95% confident that the reasoning is correct?
> 
> This is not how reasoning work.

This is not how some particular form of reasoning works.
But I have read about ideas that even formal reasoning could exist in forms that trade efficiency against correctness. Think of it as an analog of, say, image processing algorithms, which also can trade speed against resolution.
So you could have your program and various (continuous?) ways of choosing between fast and exact and maybe your particular program is so complex that exact reasoning would take more than a lifetime, whereas a reasonably high level of confidence (but <100%) could be achieved in a timeframe that is acceptable for you and your customer.
What would you do?

Today you just ditch formal methods whatsoever and go on with laborious testing. As if that was any wiser.

> But human reasoning is nowhere stochastic.

Paul asked for machine verification, so the limitations of human reasoning need not bother us.

> BTW, a digital system has an advantage that you can (theoretically) 
> ensure some states never entered.

But I'm not talking about system states, but about our confidence that a given state will be achieved or not. States can be discrete, but confidence (and therefore so called "certification credit") might have a continuous measure. Of course, we don't yet have the formal methods with such capability, but maybe the methods we have now are not fit for what we are trying to do with them anyway.

-- 
Maciej Sobczak * http://www.inspirel.com

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29  6:57                                           ` Maciej Sobczak
@ 2019-03-29  7:13                                             ` Paul Rubin
  2019-03-29  8:39                                             ` Dmitry A. Kazakov
  1 sibling, 0 replies; 146+ messages in thread
From: Paul Rubin @ 2019-03-29  7:13 UTC (permalink / raw)


Maciej Sobczak <see.my.homepage@gmail.com> writes:
> Paul asked for machine verification, so the limitations of human
> reasoning need not bother us.

Systems like SPARK don't do any significant amount of automatic
reasoning.  You do the reasoning in your own head in the usual way.
SPARK them lets you write the reasoning down in a precise enough way
that the verifier can check it.  It's just like how the Ada compiler (or
some other programming language) lets you write down the computational
steps of your algorithm in a precise enough way that the machine can
execute it.

> a continuous measure. Of course, we don't yet have the formal methods
> with such capability, 

Sure we do.  For example, probabilistic algorithms are a thing.  Or you
could prove that with a given distribution of input values, your
algorithm will succeed 98.235% of the time.  There might be some kinds
of tasks for which that is sufficient, especially if you can detect the
failed instances and reprocess them.

Usually though, one resorts to formal methods in order to eliminate as
much uncertainty as possible.  So if you need a bounded WCET you won't
use a hash table, or that type of thing.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29  5:13                                             ` Bojan Bozovic
@ 2019-03-29  8:13                                               ` Dmitry A. Kazakov
  0 siblings, 0 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-29  8:13 UTC (permalink / raw)


On 2019-03-29 06:13, Bojan Bozovic wrote:
> On Thursday, March 28, 2019 at 9:48:09 PM UTC+1, G. B. wrote:
>> Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
>>> On 2019-03-28 08:01, Maciej Sobczak wrote:
>>> Attempts to use quality assurance
>>> methods known in engineering disciplines to software result in
>>> nonsensical standards and certification procedures which assure nothing
>>> but wasting human resources.
>>>
>>
>> The equivalence class of economically viable software firms demonstrates
>> that there exist a sweet spot. It lies between investing in the production
>> of correct logic and selling software that has layers of waste.
>>
>> For an analogy, compare compost and composites.
>>
>> Customers and programmers alike might say that anything with waste in it is
>> not sweet, it’s bitter. But, they are sheep. Enjoy Ada while you can.
> 
> With Internet of Things and the like devices, self-driving cars etc. the need for correctness in software will only increase not otherwise. When computers can affect the environment physically matter of correct behaviour becomes paramount, so Ada really have the future. What's important is to promote it outside of safety-critical software, for general programming, so that those that don't even know about Ada now can learn it and use it.

Software of this kind is practically non-testable. In mechanical 
engineering with its differentiable functions and linear approximations 
of, you can test for extreme points and deduce the rest working. So the 
car crash tests go. With software and especially with decision making 
tasks that approach is doomed. You can die at any "speed" just same. 
Thus correctness proofs is the only tool left.

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29  6:57                                           ` Maciej Sobczak
  2019-03-29  7:13                                             ` Paul Rubin
@ 2019-03-29  8:39                                             ` Dmitry A. Kazakov
  2019-04-01 15:13                                               ` Optikos
  1 sibling, 1 reply; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-03-29  8:39 UTC (permalink / raw)


On 2019-03-29 07:57, Maciej Sobczak wrote:

> But I have read about ideas that even formal reasoning could exist in forms that trade efficiency against correctness. Think of it as an analog of, say, image processing algorithms, which also can trade speed against resolution.

Each such reasoning, e.g. fuzzy or probabilistic inference can be 
reduced to a crisp reasoning about imprecise statements. E.g. a proof 
that the probability of E is greater than X.

> So you could have your program and various (continuous?) ways of choosing between fast and exact and maybe your particular program is so complex that exact reasoning would take more than a lifetime, whereas a reasonably high level of confidence (but <100%) could be achieved in a timeframe that is acceptable for you and your customer.

No, you cannot. You can prove weaker propositions but that is not same. 
There is no continuum of proofs. There might be some of propositions 
depending on the nature of things they state, in some few cases...

> What would you do?
> 
> Today you just ditch formal methods whatsoever and go on with laborious testing. As if that was any wiser.

Right, but it is not a question of half-proofs about the same thing. 
IMO, the solution is proofs about things that can be proved leaving 
intractable issues aside.

I always wished SPARK integrated into Ada allowing the programmer to 
choose what to prove at the programming unit level without limiting the 
language.

This especially applies to pointers. Leave them alone! There is no need 
in accessibility checks or any limitations and ownership schemes. Just 
give exception contracts and let me prove no Constraint_Error 
propagating. Job done.

>> But human reasoning is nowhere stochastic.
> 
> Paul asked for machine verification, so the limitations of human reasoning need not bother us.
> 
>> BTW, a digital system has an advantage that you can (theoretically)
>> ensure some states never entered.
> 
> But I'm not talking about system states, but about our confidence that a given state will be achieved or not. States can be discrete, but confidence (and therefore so called "certification credit") might have a continuous measure.

That measure is useless as it does not apply to the system in question. 
This by the way is the MAJOR flaw of certification procedures. The 
measure (confidence factor) applies to the *certifier*. It tells how 
much you managed to hide system faults from him.

> Of course, we don't yet have the formal methods with such capability, but maybe the methods we have now are not fit for what we are trying to do with them anyway.

There is a mountain of papers regarding confidence factors and their 
application. The only problem in connection to software design is that 
they are a measure of confidence in what you think rather than in what 
actually is.

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


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-11 22:08   ` Jeffrey R. Carter
  2019-03-12  2:04     ` Lucretia
  2019-03-13  9:10     ` Maciej Sobczak
@ 2019-03-29 17:38     ` Florian Weimer
  2 siblings, 0 replies; 146+ messages in thread
From: Florian Weimer @ 2019-03-29 17:38 UTC (permalink / raw)


* Jeffrey R. Carter:

> On 3/11/19 4:34 PM, Lucretia wrote:
>  > On Friday, 8 March 2019 16:43:50 UTC, Olivier Henley  wrote:
>  >> Maybe someone with all the proper ammunitions could enlighten this user:
>  >>
>  >> https://users.rust-lang.org/t/if-ada-is-already-very-safe-why-rust/21911/11
>  >
>  > Just tore them a new one :)
>
> As far as I can see, Rust's only innovation is safer pointers, but
> it still has a bad design that requires the use of pointers. In Ada,
> pointers are never needed.* So Ada is still safer when dealing with
> pointers, since you never need to.

This argument is not valid because Ada does not provide type safety,
even in the absence of pointers, pragmas, representation clauses, or
use of library facilities.

I think it's difficult to dismiss Rust's type system and claim that
Ada's approach is superior.  The arguments will look a lot like those
that programmers who prefer C to Ada bring forward.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-12 21:53             ` Randy Brukardt
  2019-03-13 10:50               ` Jere
  2019-03-17 12:52               ` Optikos
@ 2019-03-29 17:41               ` Florian Weimer
  2019-03-29 22:16                 ` Randy Brukardt
  2 siblings, 1 reply; 146+ messages in thread
From: Florian Weimer @ 2019-03-29 17:41 UTC (permalink / raw)


* Randy Brukardt:

> It's also possible that Ada 2020 will have a form of pointer ownership. 
> (Unfortunately, we didn't make any conclusions on that during yesterday's 
> meeting, so it's still in limbo, and we're getting very close to the finish 
> line.)

What about other holes in the type system?  Aliasing can occur in
function calls even without pointers.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-18 23:36                 ` Randy Brukardt
  2019-03-19  2:18                   ` Optikos
@ 2019-03-29 17:56                   ` Florian Weimer
  2019-03-29 22:17                     ` Randy Brukardt
  1 sibling, 1 reply; 146+ messages in thread
From: Florian Weimer @ 2019-03-29 17:56 UTC (permalink / raw)


* Randy Brukardt:

> But a better question is whether the Rust borrow checker allows
> building proper ADTs for most data structures.

The Rust standard library uses unsafe extensively in the
implementation of containers.  I'm not sure if this is a problem.
Most languages have this property (that the standard library cannot be
implemented in the language itself).

For container libraries, the only widely-used counter-example (of
which I'm aware) is pre-generic Java.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29 17:41               ` Florian Weimer
@ 2019-03-29 22:16                 ` Randy Brukardt
  2019-03-29 22:43                   ` Florian Weimer
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-29 22:16 UTC (permalink / raw)


"Florian Weimer" <fw@deneb.enyo.de> wrote in message 
news:87wokhk289.fsf@mid.deneb.enyo.de...
>* Randy Brukardt:
>
>> It's also possible that Ada 2020 will have a form of pointer ownership.
>> (Unfortunately, we didn't make any conclusions on that during yesterday's
>> meeting, so it's still in limbo, and we're getting very close to the 
>> finish
>> line.)
>
> What about other holes in the type system?  Aliasing can occur in
> function calls even without pointers.

No one submitted any problems in that area (and I don't see why "aliasing" 
equates to "a hole in the type system" anyway).

Personally, I don't think it is possible to meet the goals for efficiency 
without aliasing -- one would have to eliminate things like by-reference 
parameter passing and techniques like lookup indexes to avoid aliasing. That 
sort of thing is pointless, at least when performance (time/space/power) 
matter.

One can always chose to use Ada in a functional manner (by requiring single 
assignment and the like), but I don't think that functional programming of 
that sort is practical for larger programs.

                                           Randy.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29 17:56                   ` Florian Weimer
@ 2019-03-29 22:17                     ` Randy Brukardt
  2019-03-29 22:35                       ` Florian Weimer
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-03-29 22:17 UTC (permalink / raw)


>"Florian Weimer" <fw@deneb.enyo.de> wrote in message 
>news:87sgv5k1j5.fsf@mid.deneb.enyo.de...
>* Randy Brukardt:
>
>> But a better question is whether the Rust borrow checker allows
>> building proper ADTs for most data structures.
>
> The Rust standard library uses unsafe extensively in the
> implementation of containers.  I'm not sure if this is a problem.
> Most languages have this property (that the standard library cannot be
> implemented in the language itself).
>
> For container libraries, the only widely-used counter-example (of
> which I'm aware) is pre-generic Java.

You're saying Ada isn't widely used? And I thought the STL was implemented 
in C++.

                                Randy.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29 22:17                     ` Randy Brukardt
@ 2019-03-29 22:35                       ` Florian Weimer
  2019-04-01 21:17                         ` Randy Brukardt
  0 siblings, 1 reply; 146+ messages in thread
From: Florian Weimer @ 2019-03-29 22:35 UTC (permalink / raw)


* Randy Brukardt:

>>"Florian Weimer" <fw@deneb.enyo.de> wrote in message 
>>news:87sgv5k1j5.fsf@mid.deneb.enyo.de...
>>* Randy Brukardt:
>>
>>> But a better question is whether the Rust borrow checker allows
>>> building proper ADTs for most data structures.
>>
>> The Rust standard library uses unsafe extensively in the
>> implementation of containers.  I'm not sure if this is a problem.
>> Most languages have this property (that the standard library cannot be
>> implemented in the language itself).
>>
>> For container libraries, the only widely-used counter-example (of
>> which I'm aware) is pre-generic Java.
>
> You're saying Ada isn't widely used? And I thought the STL was implemented 
> in C++.

The GNAT implementation doesn't seem particularly memory-safe to me,
looking at Ada.Containers.Bounded_Ordered_Maps (which picked more or
less at random).


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29 22:16                 ` Randy Brukardt
@ 2019-03-29 22:43                   ` Florian Weimer
  2019-04-01 21:29                     ` Randy Brukardt
  0 siblings, 1 reply; 146+ messages in thread
From: Florian Weimer @ 2019-03-29 22:43 UTC (permalink / raw)


* Randy Brukardt:

> "Florian Weimer" <fw@deneb.enyo.de> wrote in message 
> news:87wokhk289.fsf@mid.deneb.enyo.de...
>>* Randy Brukardt:
>>
>>> It's also possible that Ada 2020 will have a form of pointer ownership.
>>> (Unfortunately, we didn't make any conclusions on that during yesterday's
>>> meeting, so it's still in limbo, and we're getting very close to the 
>>> finish
>>> line.)
>>
>> What about other holes in the type system?  Aliasing can occur in
>> function calls even without pointers.
>
> No one submitted any problems in that area (and I don't see why "aliasing" 
> equates to "a hole in the type system" anyway).

It's supposed to be quite well-known (Robert A Duff recognized it in
2011 and provided the Ada 83 reference):

generic
   type Source is private;
   type Target is private;
function Conversion (S : Source) return Target;

function Conversion (S : Source) return Target is
   type Source_Wrapper is tagged record
      S : Source;
   end record;
   type Target_Wrapper is tagged record
      T : Target;
   end record;
   
   type Selector is (Source_Field, Target_Field);
   type Magic (Sel : Selector := Target_Field) is record
      case Sel is
	 when Source_Field =>
	    S : Source_Wrapper;
	 when Target_Field =>
	    T : Target_Wrapper;
      end case;
   end record;
   
   M : Magic;
   
   function Convert (T : Target_Wrapper) return Target is
   begin
      M := (Sel => Source_Field, S => (S => S));
      return T.T;
   end Convert;
   
begin
   return Convert (M.T);
end Conversion;

> Personally, I don't think it is possible to meet the goals for efficiency 
> without aliasing -- one would have to eliminate things like by-reference 
> parameter passing and techniques like lookup indexes to avoid aliasing.

It might be sufficient to check for aliasing when passing parameters
and raise Program_Error.

> That sort of thing is pointless, at least when performance
> (time/space/power) matter.

We'll see how Rust works this out over the coming years.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-28  8:39                                           ` Simon Wright
@ 2019-03-30  4:31                                             ` Paul Rubin
  0 siblings, 0 replies; 146+ messages in thread
From: Paul Rubin @ 2019-03-30  4:31 UTC (permalink / raw)


Simon Wright <simon@pushface.org> writes:
> https://youtu.be/DnsLpEgFUSk I think. Only the slides, I think, but the
> voice is distinctive!

That looks interesting and I'll try to watch it sometime, but it's not
the one I remember.  I found it here ("Ada, Past Present and Future"):

  https://youtu.be/0yXwnk8Cr0c?t=2218

The talk wasn't purely about the F-22.  It was about Ada in general, and
the F-22 came up at some point in it.  

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-28  7:17                                         ` Paul Rubin
  2019-03-28  8:39                                           ` Simon Wright
@ 2019-03-30 22:14                                           ` Robert A Duff
  2019-03-30 22:55                                             ` Paul Rubin
  1 sibling, 1 reply; 146+ messages in thread
From: Robert A Duff @ 2019-03-30 22:14 UTC (permalink / raw)


Paul Rubin <no.email@nospam.invalid> writes:

> Fwiw, there's a video on Youtube of Adacore founder Bob Dewar talking

Robert Dewar.  He would say, were he still alive, "Bob is a nice
name, but it's not my name."

- Bob

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-30 22:14                                           ` Robert A Duff
@ 2019-03-30 22:55                                             ` Paul Rubin
  0 siblings, 0 replies; 146+ messages in thread
From: Paul Rubin @ 2019-03-30 22:55 UTC (permalink / raw)


Robert A Duff <bobduff@TheWorld.com> writes:
> Robert Dewar.  He would say, were he still alive, "Bob is a nice
> name, but it's not my name."

Thanks.  I exchanged some email with him once about SPITBOL but sadly I
never met him.  I had a question for him about one of his GNAT-related
GCC mailing list posts that I had hoped to ask him at a suitable
opportunity, but I missed my chance.  It's been weighing on me since
then too.  RIP Robert.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-08 16:43 Olivier Henley
                   ` (4 preceding siblings ...)
  2019-03-22 11:10 ` Lucretia
@ 2019-04-01  7:28 ` gautier_niouzes
  5 siblings, 0 replies; 146+ messages in thread
From: gautier_niouzes @ 2019-04-01  7:28 UTC (permalink / raw)


Next one ;-) ?

https://lemire.me/blog/2019/03/28/java-is-not-a-safe-language/


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29  8:39                                             ` Dmitry A. Kazakov
@ 2019-04-01 15:13                                               ` Optikos
  2019-04-01 16:51                                                 ` Dmitry A. Kazakov
  0 siblings, 1 reply; 146+ messages in thread
From: Optikos @ 2019-04-01 15:13 UTC (permalink / raw)


On Friday, March 29, 2019 at 4:39:13 AM UTC-4, Dmitry A. Kazakov wrote:
> On 2019-03-29 07:57, Maciej Sobczak wrote:
> 
> > But I have read about ideas that even formal reasoning could exist in forms that trade efficiency against correctness. Think of it as an analog of, say, image processing algorithms, which also can trade speed against resolution.
> 
> Each such reasoning, e.g. fuzzy or probabilistic inference can be 
> reduced to a crisp reasoning about imprecise statements. E.g. a proof 
> that the probability of E is greater than X.
> 
> > So you could have your program and various (continuous?) ways of choosing between fast and exact and maybe your particular program is so complex that exact reasoning would take more than a lifetime, whereas a reasonably high level of confidence (but <100%) could be achieved in a timeframe that is acceptable for you and your customer.
> 
> No, you cannot. You can prove weaker propositions but that is not same. 
> There is no continuum of proofs. There might be some of propositions 
> depending on the nature of things they state, in some few cases...
> 
> > What would you do?
> > 
> > Today you just ditch formal methods whatsoever and go on with laborious testing. As if that was any wiser.
> 
> Right, but it is not a question of half-proofs about the same thing. 
> IMO, the solution is proofs about things that can be proved leaving 
> intractable issues aside.
> 
> I always wished SPARK integrated into Ada allowing the programmer to 
> choose what to prove at the programming unit level without limiting the 
> language.
> 
> This especially applies to pointers. Leave them alone! There is no need 
> in accessibility checks or any limitations and ownership schemes. Just 
> give exception contracts and let me prove no Constraint_Error 
> propagating. Job done.

Dmitry, I agree with nearly everything in reply to Maciej Sobczak on this thread—perhaps everything, depending on your answer to the following.  One clarifying question that I have is:  how would you “prove no Constraint_Error propagating”?  At run-time or at compile-time or at engineering-time using tools other than the compiler?

If at compile-time or at engineering-time using tools other than the compiler, then that is the solution that ATS2 and ATS3 are pursuing, where ATS's type views are rough analogues of what you are calling exception contracts here.

Paul Rubin,  again thank you for the ATS tip.  It is almost precisely what I have been looking for.  I've been having a blast learning ATS2 (and trying to discern what is emerging in the ATS3 under development).  SML meh.  Haskell: meh.  OCaml: better but still meh.  MetaCaml: fascinating but still meh.  Coq not tightly integrated into OCaml:  meh.  ATS2+ATS/LF now that is more like what I had in mind: rather smooth integration of multi-paradigm dynamic programming language with VDM-esque/Z-esque (zed) stepwise refinement with theorem prover with pointer correctness via type views.

> >> But human reasoning is nowhere stochastic.
> > 
> > Paul asked for machine verification, so the limitations of human reasoning need not bother us.
> > 
> >> BTW, a digital system has an advantage that you can (theoretically)
> >> ensure some states never entered.
> > 
> > But I'm not talking about system states, but about our confidence that a given state will be achieved or not. States can be discrete, but confidence (and therefore so called "certification credit") might have a continuous measure.
> 
> That measure is useless as it does not apply to the system in question. 
> This by the way is the MAJOR flaw of certification procedures. The 
> measure (confidence factor) applies to the *certifier*. It tells how 
> much you managed to hide system faults from him.

Amen.  Certification of the people obfuscating software flaws, not certification of the software, is what most certifications arrive at in the end.  Bless their heart, their goals were almost correct, but without the (semi-automated!) formal mathematical proofs at the foundation of the process, quality certification is a fool's errand of people looking good, instead of making the software actually defect free.

> > Of course, we don't yet have the formal methods with such capability, but maybe the methods we have now are not fit for what we are trying to do with them anyway.
> 
> There is a mountain of papers regarding confidence factors and their 
> application. The only problem in connection to software design is that 
> they are a measure of confidence in what you think rather than in what 
> actually is.
> 
> -- 
> Regards,
> Dmitry A. Kazakov
> http://www.dmitry-kazakov.de


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-01 15:13                                               ` Optikos
@ 2019-04-01 16:51                                                 ` Dmitry A. Kazakov
  2019-04-01 21:42                                                   ` Randy Brukardt
  0 siblings, 1 reply; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-04-01 16:51 UTC (permalink / raw)


On 2019-04-01 17:13, Optikos wrote:

>  One clarifying question that I have is:  how would you “prove no Constraint_Error propagating”?  At run-time or at compile-time or at engineering-time using tools other than the compiler?

It must be the compiler. The programmer states contracts of the 
subprograms and if the contracts cannot be proven to hold that is a 
compile-time error.

The problem is, of course, specifying the mandatory strength of a proof 
AKA false negatives vs. false positives. If a fact cannot be proven true 
by one compiler that makes the program illegal even if another compiler 
could prove it.

E.g. in the current Ada the program

    function Foo return Integer is
    begin
       raise Data_Error;
    end Foo;

is illegal, though every compiler can prove its equivalence to the legal 
one:

    function Foo return Integer is
    begin
       raise Data_Error;
       return 0;
    end Foo;

One way out could be user provided axioms which the compiler is allowed 
to use when it fails to find a proof (with a warning of course):

    function Foo return Integer is
    begin
       raise Data_Error;
## I swear there is a return statement
    end Foo;

> If at compile-time or at engineering-time using tools other than the compiler, then that is the solution that ATS2 and ATS3 are pursuing, where ATS's type views are rough analogues of what you are calling exception contracts here.

Exception contracts are not related to types. But otherwise, yes, SPARK 
must be integrated into Ada.

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


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29 22:35                       ` Florian Weimer
@ 2019-04-01 21:17                         ` Randy Brukardt
  0 siblings, 0 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-04-01 21:17 UTC (permalink / raw)


"Florian Weimer" <fw@deneb.enyo.de> wrote in message 
news:87zhpdgvhl.fsf@mid.deneb.enyo.de...
>* Randy Brukardt:
>
>>>"Florian Weimer" <fw@deneb.enyo.de> wrote in message
>>>news:87sgv5k1j5.fsf@mid.deneb.enyo.de...
>>>* Randy Brukardt:
>>>
>>>> But a better question is whether the Rust borrow checker allows
>>>> building proper ADTs for most data structures.
>>>
>>> The Rust standard library uses unsafe extensively in the
>>> implementation of containers.  I'm not sure if this is a problem.
>>> Most languages have this property (that the standard library cannot be
>>> implemented in the language itself).
>>>
>>> For container libraries, the only widely-used counter-example (of
>>> which I'm aware) is pre-generic Java.
>>
>> You're saying Ada isn't widely used? And I thought the STL was 
>> implemented
>> in C++.
>
> The GNAT implementation doesn't seem particularly memory-safe to me,
> looking at Ada.Containers.Bounded_Ordered_Maps (which picked more or
> less at random).

You said "Most languages have this property (that the standard library 
cannot be implemented in the language itself)." You didn't say anything 
about memory safety -- and it wouldn't make sense anyway, since most 
languages don't have "memory safety" (whatever that is) in the first place.

For Ada, the entire idea of the containers was to allow implementations to 
have as much (or as little) memory safety as they want. There's none that an 
implementation can provide with access types.

                               Randy. 



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-03-29 22:43                   ` Florian Weimer
@ 2019-04-01 21:29                     ` Randy Brukardt
  2019-04-01 22:14                       ` Simon Wright
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-04-01 21:29 UTC (permalink / raw)


"Florian Weimer" <fw@deneb.enyo.de> wrote in message 
news:87va01gv3t.fsf@mid.deneb.enyo.de...
...
>> Personally, I don't think it is possible to meet the goals for efficiency
>> without aliasing -- one would have to eliminate things like by-reference
>> parameter passing and techniques like lookup indexes to avoid aliasing.
>
> It might be sufficient to check for aliasing when passing parameters
> and raise Program_Error.

??? The parameter itself is the problem. Any call would have to raise 
Program_Error in such a case.

The only way to make such a check that wouldn't trigger all of the time 
would require looking at both the body and the call at the same time -- a 
complete abandonment of privacy and separation of concerns.

The problem in your example is the object with mutable discriminants. As 
soon as those exist, it's very difficult to prevent such problems. The 
"obvious" solution is to ban such types, or ban (as is done for renames) 
passing any such components as parameters. Neither would be remotely 
compatible or possible for Ada.

In any case, I don't see discriminant-dependent components as having 
anything to do with violating the type model. You seem to expect more out of 
the type model than I do! This is just one of many ways to cause erroneous 
execution in Ada. A "perfect" language would have no such ways, but those 
are allowed in Ada as a compromise between perfect checking and performance.

                                                   Randy.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-01 16:51                                                 ` Dmitry A. Kazakov
@ 2019-04-01 21:42                                                   ` Randy Brukardt
  2019-04-02  8:30                                                     ` Dmitry A. Kazakov
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-04-01 21:42 UTC (permalink / raw)


"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:q7tfi3$1483$1@gioia.aioe.org...
> On 2019-04-01 17:13, Optikos wrote:
>
>>  One clarifying question that I have is:  how would you "prove no 
>> Constraint_Error propagating"?  At run-time or at compile-time or at 
>> engineering-time using tools other than the compiler?
>
> It must be the compiler. The programmer states contracts of the 
> subprograms and if the contracts cannot be proven to hold that is a 
> compile-time error.
>
> The problem is, of course, specifying the mandatory strength of a proof 
> AKA false negatives vs. false positives. If a fact cannot be proven true 
> by one compiler that makes the program illegal even if another compiler 
> could prove it.

The problem with that is that in the canonical Ada description, it's always 
possible for a check to fail. One would need to describe in precise terms 
what "optimizations" of checks that a compiler is mandated to do, or the 
"proof" would be pointless. That is, in the hypothetical:

    function Foo return Natural
         with Exceptions => null is (0);

this is illegal in the general case, since this function can raise 
Constraint_Error (from the conversion of the literal to Natural) and 
Storage_Error (since everything can raise Storage_Error).

One could imagine trying to invent a set of rules of which check 
optimizations have to be made (a conversion of a literal to a subtype only 
raises an exception if it actually out of range; a conversion of an object 
of a subtype to the same subtype never raises an exceptions; and so on), but 
such a set of rules would either be massive and put a lot of burden on 
compilers (especially existing compilers), or would be full of holes and 
thus little could be written this way.

My preference for this check is to make it implementation-defined (possibly 
with a few minimum requirements). Thus, one compiler might be able to 
compile Foo and another would not -- but it would reflect reality. A 
compiler that is smarter about checks would be able to handle more code, all 
the way up to the level of SPARK (where most code could be proved to not 
raise exceptions).

For Janus/Ada, I'm working toward having (optional) warnings for the raise 
of any exception; that, combined with warnings-as-error mode can give the 
effect of preventing any exceptions other than ones explicitly expected. 
It's pretty much all that can be done within Ada as it stands. But that is 
not as good as an exception contract (especially as exceptions that you want 
to raise become a pain).

                                                 Randy.



^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-01 21:29                     ` Randy Brukardt
@ 2019-04-01 22:14                       ` Simon Wright
  2019-04-02 21:55                         ` Randy Brukardt
  0 siblings, 1 reply; 146+ messages in thread
From: Simon Wright @ 2019-04-01 22:14 UTC (permalink / raw)


"Randy Brukardt" <randy@rrsoftware.com> writes:

> The only way to make such a check that wouldn't trigger all of the
> time would require looking at both the body and the call at the same
> time -- a complete abandonment of privacy and separation of concerns.

But it would be the compiler looking, not me.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-01 21:42                                                   ` Randy Brukardt
@ 2019-04-02  8:30                                                     ` Dmitry A. Kazakov
  2019-04-02 15:53                                                       ` Anh Vo
  0 siblings, 1 reply; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-04-02  8:30 UTC (permalink / raw)


On 2019-04-01 23:42, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:q7tfi3$1483$1@gioia.aioe.org...
>> On 2019-04-01 17:13, Optikos wrote:
>>
>>>   One clarifying question that I have is:  how would you "prove no
>>> Constraint_Error propagating"?  At run-time or at compile-time or at
>>> engineering-time using tools other than the compiler?
>>
>> It must be the compiler. The programmer states contracts of the
>> subprograms and if the contracts cannot be proven to hold that is a
>> compile-time error.
>>
>> The problem is, of course, specifying the mandatory strength of a proof
>> AKA false negatives vs. false positives. If a fact cannot be proven true
>> by one compiler that makes the program illegal even if another compiler
>> could prove it.
> 
> The problem with that is that in the canonical Ada description, it's always
> possible for a check to fail. One would need to describe in precise terms
> what "optimizations" of checks that a compiler is mandated to do, or the
> "proof" would be pointless. That is, in the hypothetical:
> 
>      function Foo return Natural
>           with Exceptions => null is (0);
> 
> this is illegal in the general case, since this function can raise
> Constraint_Error (from the conversion of the literal to Natural) and
> Storage_Error (since everything can raise Storage_Error).

The conversion will have a contract not to raise if the argument is 0. 
The Storage_Error contract will be conditional: no Storage_Error when 
stack has N free storage units free. You could then prove the program is 
safe with 10KB of stack.

> One could imagine trying to invent a set of rules of which check
> optimizations have to be made (a conversion of a literal to a subtype only
> raises an exception if it actually out of range; a conversion of an object
> of a subtype to the same subtype never raises an exceptions; and so on), but
> such a set of rules would either be massive and put a lot of burden on
> compilers (especially existing compilers), or would be full of holes and
> thus little could be written this way.

Sure. It will be a lot of work to contract *all* built-ins. This is 
another reason to reduce them drastically, thus my plea for a type 
system overhaul. The language core must have contracted. The libraries 
may have weaker contracts.

> My preference for this check is to make it implementation-defined (possibly
> with a few minimum requirements). Thus, one compiler might be able to
> compile Foo and another would not -- but it would reflect reality. A
> compiler that is smarter about checks would be able to handle more code, all
> the way up to the level of SPARK (where most code could be proved to not
> raise exceptions).

That is a compiler vendor POV. As a programmer I want the opposite. I 
want to be able to have proofs as a part of my program.

> For Janus/Ada, I'm working toward having (optional) warnings for the raise
> of any exception; that, combined with warnings-as-error mode can give the
> effect of preventing any exceptions other than ones explicitly expected.
> It's pretty much all that can be done within Ada as it stands. But that is
> not as good as an exception contract (especially as exceptions that you want
> to raise become a pain).

Right, and unanticipated exceptions is a major contributor of bugs in 
Ada. It is not so that exceptions cause bugs, rather bugs manifest 
themselves as exceptions. If one could contract them most of the bugs 
will not pass through the compiler.

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-02  8:30                                                     ` Dmitry A. Kazakov
@ 2019-04-02 15:53                                                       ` Anh Vo
  0 siblings, 0 replies; 146+ messages in thread
From: Anh Vo @ 2019-04-02 15:53 UTC (permalink / raw)


On Tuesday, April 2, 2019 at 1:30:25 AM UTC-7, Dmitry A. Kazakov wrote:
> On 2019-04-01 23:42, Randy Brukardt wrote:
> > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> > news:q7tfi3$1483$1@gioia.aioe.org...
> >> On 2019-04-01 17:13, Optikos wrote:
> >>
> 
> > For Janus/Ada, I'm working toward having (optional) warnings for the raise
> > of any exception; that, combined with warnings-as-error mode can give the
> > effect of preventing any exceptions other than ones explicitly expected.
> > It's pretty much all that can be done within Ada as it stands. But that is
> > not as good as an exception contract (especially as exceptions that you want
> > to raise become a pain).
> 
> Right, and unanticipated exceptions is a major contributor of bugs in 
> Ada. It is not so that exceptions cause bugs, rather bugs manifest 
> themselves as exceptions. If one could contract them most of the bugs 
> will not pass through the compiler.

Then, all bugs will be caught after they manifest themselves as exceptions. This is a brilliant idea. As the result, debugger is needed much less in the future.

Anh Vo


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-01 22:14                       ` Simon Wright
@ 2019-04-02 21:55                         ` Randy Brukardt
  2019-04-04 15:07                           ` Simon Wright
  0 siblings, 1 reply; 146+ messages in thread
From: Randy Brukardt @ 2019-04-02 21:55 UTC (permalink / raw)


"Simon Wright" <simon@pushface.org> wrote in message 
news:lywokdfk5q.fsf@pushface.org...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> The only way to make such a check that wouldn't trigger all of the
>> time would require looking at both the body and the call at the same
>> time -- a complete abandonment of privacy and separation of concerns.
>
> But it would be the compiler looking, not me.

Doesn't matter. One can't depend on the contract of a subprogram if some 
calls are going to be illegal/raise P_E because of the contents of the body. 
The whole point privacy/separation of concerns is that no one (programmers, 
tools, compilers) can see/depend on any of the details of the 
implementation -- that allows one to reason (including make proofs) about a 
call without looking in bodies (nor for those bodies to actually exist when 
the reasoning occurs). Otherwise, one can only reason about a complete 
program, which has many nasty effects (much of the reasoning occurs too 
late, when the design is already frozen and the code exists -- at that point 
it is hard to make fundamental changes).

Ada has always been pretty fanatical about privacy; abandoning that would be 
a huge deal. I'd probably say that Ada has emphasized privacy over pretty 
much everything else (including error detection). It seems unlikely that one 
can have everything -- language design has always been about such 
trade-offs.

                                                        Randy.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
@ 2019-04-02 22:07 Randy Brukardt
  2019-04-03  7:29 ` Dmitry A. Kazakov
                   ` (3 more replies)
  0 siblings, 4 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-04-02 22:07 UTC (permalink / raw)


[Header too long again. - RLB]

"Anh Vo" <anhvofrcaus@gmail.com> wrote in message
news:4b2b0543-1125-4a80-9a94-abca08e60b7d@googlegroups.com...
> On Tuesday, April 2, 2019 at 1:30:25 AM UTC-7, Dmitry A. Kazakov wrote:
>> On 2019-04-01 23:42, Randy Brukardt wrote:
>> > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> > news:q7tfi3$1483$1@gioia.aioe.org...
>> >> On 2019-04-01 17:13, Optikos wrote:
>> >>
>>
>> > For Janus/Ada, I'm working toward having (optional) warnings for the
>> > raise
>> > of any exception; that, combined with warnings-as-error mode can give
>> > the
>> > effect of preventing any exceptions other than ones explicitly
>> > expected.
>> > It's pretty much all that can be done within Ada as it stands. But that
>> > is
>> > not as good as an exception contract (especially as exceptions that you
>> > want
>> > to raise become a pain).
>>
>> Right, and unanticipated exceptions is a major contributor of bugs in
>> Ada. It is not so that exceptions cause bugs, rather bugs manifest
>> themselves as exceptions. If one could contract them most of the bugs
>> will not pass through the compiler.
>
> Then, all bugs will be caught after they manifest themselves as
> exceptions. This is
> a brilliant idea. As the result, debugger is needed much less in the
> future.

Does anyone spend much time in a debugger when writing Ada? Almost all of
the time I do it is to track down compiler bugs (hopefully something that
the average Ada user doesn't do often). With the default exception
information, there is little need to debug anything the majority of the
time.

Certainly, moving detection to compile-time is even better. But I don't see
that changing the mostly non-existent use of debuggers much.

                                                Randy.




^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-02 22:07 Randy Brukardt
@ 2019-04-03  7:29 ` Dmitry A. Kazakov
  2019-04-03 14:31   ` Optikos
  2019-04-03 15:07 ` Lucretia
                   ` (2 subsequent siblings)
  3 siblings, 1 reply; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-04-03  7:29 UTC (permalink / raw)


On 2019-04-03 00:07, Randy Brukardt wrote:

> Does anyone spend much time in a debugger when writing Ada?

Well if there were a working one. GDB does not count.

I am using tracing, but there are few cases where debugger could be 
easier to use. In the debugger you could inspect the states of variables 
and of other tasks. And you don't need to modify the code. It is quite 
often that I have to add, in addition to "standard" tracing, some more 
extensive tracing which I remove later.

> Almost all of
> the time I do it is to track down compiler bugs (hopefully something that
> the average Ada user doesn't do often). With the default exception
> information, there is little need to debug anything the majority of the
> time.

In some cases there is a long way to the exception. The most infamous 
case is an exception in the Finalize caused by attempted automatic 
finalization of dangling objects, which must not be there at all.

(I mean both the dangling objects and finalization lists of! (:-))

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03  7:29 ` Dmitry A. Kazakov
@ 2019-04-03 14:31   ` Optikos
  2019-04-03 14:54     ` Dmitry A. Kazakov
  0 siblings, 1 reply; 146+ messages in thread
From: Optikos @ 2019-04-03 14:31 UTC (permalink / raw)


On Wednesday, April 3, 2019 at 3:29:22 AM UTC-4, Dmitry A. Kazakov wrote:
> On 2019-04-03 00:07, Randy Brukardt wrote:
> 
> > Does anyone spend much time in a debugger when writing Ada?
> 
> Well if there were a working one. GDB does not count.
> 
> I am using tracing, but there are few cases where debugger could be 
> easier to use. In the debugger you could inspect the states of variables 
> and of other tasks. And you don't need to modify the code.

Which feature(s) [that other debuggers have] do you think are missing from GDB when debugging Ada?  Which are the better-than-GDB debuggers for Ada that you have seen?


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 14:31   ` Optikos
@ 2019-04-03 14:54     ` Dmitry A. Kazakov
  2019-04-03 15:29       ` Optikos
  2019-04-03 16:16       ` Simon Wright
  0 siblings, 2 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-04-03 14:54 UTC (permalink / raw)


On 2019-04-03 16:31, Optikos wrote:

> Which feature(s) [that other debuggers have] do you think are missing from GDB when debugging Ada?

Other debuggers work, GDB does not. If you have an Ada project of a 
moderate size GDB stops working.

> Which are the better-than-GDB debuggers for Ada that you have seen?

Anything is better. VMS debugger was excellent. MS Visual Studio 
debugger is OK (ObjectAda used MS format, so that Ada could be debugged 
using the MS debugger).

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


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-02 22:07 Randy Brukardt
  2019-04-03  7:29 ` Dmitry A. Kazakov
@ 2019-04-03 15:07 ` Lucretia
  2019-04-03 16:15   ` Simon Wright
  2019-04-03 17:23 ` Niklas Holsti
  2019-04-03 18:58 ` Dennis Lee Bieber
  3 siblings, 1 reply; 146+ messages in thread
From: Lucretia @ 2019-04-03 15:07 UTC (permalink / raw)


On Tuesday, 2 April 2019 23:07:26 UTC+1, Randy Brukardt  wrote:

> Does anyone spend much time in a debugger when writing Ada? Almost all of

Only when messing with memory, allocations, deletions, etc. or pointers.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 14:54     ` Dmitry A. Kazakov
@ 2019-04-03 15:29       ` Optikos
  2019-04-03 16:16       ` Simon Wright
  1 sibling, 0 replies; 146+ messages in thread
From: Optikos @ 2019-04-03 15:29 UTC (permalink / raw)


On Wednesday, April 3, 2019 at 10:54:04 AM UTC-4, Dmitry A. Kazakov wrote:
> On 2019-04-03 16:31, Optikos wrote:
> 
> > Which feature(s) [that other debuggers have] do you think are missing from GDB when debugging Ada?
> 
> Other debuggers work, GDB does not. If you have an Ada project of a 
> moderate size GDB stops working.

Fascinating, that might explain some of Ada's lack of increasing popularity.
1) Is this bug across all variants of GNAT?
1.1) paid-support AdaCore GNAT Pro?
1.2) AdaCore GPL-edition GNAT?
1.3) FSF GNAT?
1.4) All recent versions?
2) Is the bug observable both
2.1) in GDB-API/ABI-based Eclipse+GNATbench and
2.2) in stand-alone real FSF GDB?
3) Is the bug observable both
3.1) in normal symbols-in-the-object-code mode as well as
3.2) remote debugging with symbols only back on the mothership?
4) Has anyone reported it officially?
4.1) If so, what was the response (or lack thereof)?
5) Is it reproducible 100% of the time with Ada source code of size X?
5.1) How big is X?
5.2) Is X measured in raw size (e.g., kilobytes of source code)?
5.3) Or is X measured in density of complexity (e.g., quantity of sophisticated features intertwined within one/few localities)?

And due to the relatively narrow window of time, no one probably used the old DragonEgg with LLVM backend enough to know whether the bug is observable in a drastically different back-end (i.e., lldb).

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 15:07 ` Lucretia
@ 2019-04-03 16:15   ` Simon Wright
  0 siblings, 0 replies; 146+ messages in thread
From: Simon Wright @ 2019-04-03 16:15 UTC (permalink / raw)


Lucretia <laguest9000@googlemail.com> writes:

> On Tuesday, 2 April 2019 23:07:26 UTC+1, Randy Brukardt  wrote:
>
>> Does anyone spend much time in a debugger when writing Ada? Almost
>> all of
>
> Only when messing with memory, allocations, deletions, etc. or
> pointers.

Or interfacing with other languages. (which, most of the time, comes
down to Luke's list). Or on an MCU, which tends to be a combination of
the above!

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 14:54     ` Dmitry A. Kazakov
  2019-04-03 15:29       ` Optikos
@ 2019-04-03 16:16       ` Simon Wright
  2019-04-03 17:15         ` Dmitry A. Kazakov
  1 sibling, 1 reply; 146+ messages in thread
From: Simon Wright @ 2019-04-03 16:16 UTC (permalink / raw)


"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

>> Which feature(s) [that other debuggers have] do you think are
>> missing from GDB when debugging Ada?
>
> Other debuggers work, GDB does not. If you have an Ada project of a
> moderate size GDB stops working.

How big is "moderate"?


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 16:16       ` Simon Wright
@ 2019-04-03 17:15         ` Dmitry A. Kazakov
  2019-04-03 21:12           ` Simon Wright
                             ` (2 more replies)
  0 siblings, 3 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-04-03 17:15 UTC (permalink / raw)


On 2019-04-03 18:16, Simon Wright wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>>> Which feature(s) [that other debuggers have] do you think are
>>> missing from GDB when debugging Ada?
>>
>> Other debuggers work, GDB does not. If you have an Ada project of a
>> moderate size GDB stops working.
> 
> How big is "moderate"?

In none of my projects GDB works. I never tried to figure out if that is
related to the number of compilation units or number of library projects 
involved.

When you click Debug->Initialize->your-main-program in GPS and debugger 
does not start you know you reached the point.

P.S. It never worked reliable in GPS and I bet it never will.

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-02 22:07 Randy Brukardt
  2019-04-03  7:29 ` Dmitry A. Kazakov
  2019-04-03 15:07 ` Lucretia
@ 2019-04-03 17:23 ` Niklas Holsti
  2019-04-03 17:48   ` Bill Findlay
  2019-04-03 21:01   ` Simon Wright
  2019-04-03 18:58 ` Dennis Lee Bieber
  3 siblings, 2 replies; 146+ messages in thread
From: Niklas Holsti @ 2019-04-03 17:23 UTC (permalink / raw)


On 19-04-03 01:07 , Randy Brukardt wrote:

> Does anyone spend much time in a debugger when writing Ada?

I don't. I can't remember when I last used gdb or any other debugger, 
and in my ~30 years of Ada use I estimate that I have used a debugger on 
perhaps ten occasions. I have slightly more often used "monitor" 
programs to examine and alter memory and register contents when 
analysing problems in embedded programs, and those monitor programs can 
perhaps be considered crude debuggers. However, these cases involved the 
effects and meanings of HW control registers rather than ordinary 
program variables.

A propos, the name "debugger" is IMO one of the unfortunate historical 
misnomers in the programming domain. It is a misnomer because a 
"debugger" like gdb should certainly not be our main tool for removing 
bugs from programs. Diving into the debugger as the first step of 
analysing a program failure is akin to starting a new project by diving 
into coding and skipping the design phase. Moreover, the activity of 
removing a bug from program, which should be the meaning of the term 
"debugging", should certainly not consist just of a gdb/debugger session.

On the few occasions when I have used gdb or other debuggers, they have 
usually failed to help me understand the problem. The "interactive 
debugging" sessions have usually been frustrating. It is simply very 
hard to examine, understand and control the large, dynamic, complex 
beast that is the state of a program in execution, through the 
debugger's often imperfect understanding of the mapping between the 
source-level program and the machine state. Moreover, my programs are 
often real-time and multi-task and running gdb on such programs usually 
results in a quick malfunction because gdb is not in control of physical 
time.

I find, like Dmitry, that tracing and logging functions, either built 
into the program and optionally activated, or inserted ad hoc to 
understand a specific bug, are more useful. Even if the problem is not 
found in the first attempt, but needs incremental addition or activation 
of more or other logs and traces, the process is much less frustrating 
than an interactive gdb session because there is much more control, much 
less noise due to irrelevant outputs from the program and the debugger, 
and no confusion between source level and machine level.

However, I have not had access to any debugger with proper 
reverse-execution functions -- that is, a debugger that could show me 
not only what the program is doing "now", and what the variable values 
are "now", at the present breakpoint, but also what it was doing and 
what values the variables had in the recent or more distant past. If I 
had a debugger that could let me inspect the state of the program at any 
point in its execution, freely scanning and searching backwards as well 
as forwards in execution time, I might be tempted to try that debugger.

(Another important programming misnomer is "comments", which should 
certainly not be random off-the-cuff commentary, but should be logical 
and well thought-out rationale, motivation, description, analysis, etc. 
But I digress.)

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 17:23 ` Niklas Holsti
@ 2019-04-03 17:48   ` Bill Findlay
  2019-04-03 21:01   ` Simon Wright
  1 sibling, 0 replies; 146+ messages in thread
From: Bill Findlay @ 2019-04-03 17:48 UTC (permalink / raw)


On 3 Apr 2019, Niklas Holsti wrote
(in article <ggk8gpFasspU1@mid.individual.net>):

> On 19-04-03 01:07 , Randy Brukardt wrote:
>
> > Does anyone spend much time in a debugger when writing Ada?
>
> I don't. I can't remember when I last used gdb or any other debugger,
> and in my ~30 years of Ada use I estimate that I have used a debugger on
> perhaps ten occasions.

I can trump that.
I have *never* used a "debugger" in much the same time with Ada.

~30 years ago I raced an experienced programmer who was looking
for an error in his code with the DEC Ada debugger, while I
inspected his compilation listing. I won.

-- 
Bill Findlay


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-02 22:07 Randy Brukardt
                   ` (2 preceding siblings ...)
  2019-04-03 17:23 ` Niklas Holsti
@ 2019-04-03 18:58 ` Dennis Lee Bieber
  3 siblings, 0 replies; 146+ messages in thread
From: Dennis Lee Bieber @ 2019-04-03 18:58 UTC (permalink / raw)


On Tue, 2 Apr 2019 17:07:24 -0500, "Randy Brukardt" <randy@rrsoftware.com>
declaimed the following:

>Does anyone spend much time in a debugger when writing Ada? Almost all of

	I've seen people using GDB -- not necessarily for Ada (in fact,
probably not at all). I've never managed to understand GDB enough to
consider using it.

	The last debugger I used regularly (mostly for FORTRAN-77) was the one
provided by VMS; where pretty much operation relied upon it being a global
exception handler (watching variables implemented by setting the memory
page read-only, catching the attempt to write, displaying the activity, set
page to RW, update, reset to RO)...


-- 
	Wulfraed                 Dennis Lee Bieber         AF6VN
	wlfraed@ix.netcom.com    HTTP://wlfraed.home.netcom.com/ 

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 17:23 ` Niklas Holsti
  2019-04-03 17:48   ` Bill Findlay
@ 2019-04-03 21:01   ` Simon Wright
  1 sibling, 0 replies; 146+ messages in thread
From: Simon Wright @ 2019-04-03 21:01 UTC (permalink / raw)


Niklas Holsti <niklas.holsti@tidorum.invalid> writes:

> I find, like Dmitry, that tracing and logging functions, either built
> into the program and optionally activated, or inserted ad hoc to
> understand a specific bug, are more useful. Even if the problem is not
> found in the first attempt, but needs incremental addition or
> activation of more or other logs and traces, the process is much less
> frustrating than an interactive gdb session because there is much more
> control, much less noise due to irrelevant outputs from the program
> and the debugger, and no confusion between source level and machine
> level.

Agreed; in fact, we never managed to get GDB working on our VxWorks
PowerPC hardware. I don't think we seriously tried. Logging was the
thing (including exception tracebacks; unhandled exceptions were fatal,
essential in the development environment)

My part got tested on the desktop using a Tcl-based scripted testing
tool[1], which meant that I could reproduce the scenario from the logs
taken on site/at sea, demonstrate the problem, solve it (OK, sometimes
using the debugger), demonstrate the cure, & add that script to the test
suite.

[1] https://sourceforge.net/projects/scriptedtesting.coldframe.p/
    (I really need to rescue this from SF & move it to Github!)

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 17:15         ` Dmitry A. Kazakov
@ 2019-04-03 21:12           ` Simon Wright
  2019-04-04  7:09             ` Dmitry A. Kazakov
  2019-04-04  5:44           ` Maciej Sobczak
  2019-04-04 16:17           ` Optikos
  2 siblings, 1 reply; 146+ messages in thread
From: Simon Wright @ 2019-04-03 21:12 UTC (permalink / raw)


"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> In none of my projects GDB works. I never tried to figure out if that
> is related to the number of compilation units or number of library
> projects involved.
>
> When you click Debug->Initialize->your-main-program in GPS and
> debugger does not start you know you reached the point.
>
> P.S. It never worked reliable in GPS and I bet it never will.

I might well find the same if I used GPS. But there's been a lot of
trouble with GDB and macOS[1], and even after the latest fix there's
still a knack to getting GDB to start properly: see [2]. So it's
command-line only, plus swearing.

But 90% of the time it's a matter of looking at the fatal exception
traceback.

Of course, I'm not dealing with large real-time problems.

[1] https://forward-in-code.blogspot.com/2018/11/mojave-vs-gdb.html
[2] https://sourceware.org/bugzilla/show_bug.cgi?id=24069

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 17:15         ` Dmitry A. Kazakov
  2019-04-03 21:12           ` Simon Wright
@ 2019-04-04  5:44           ` Maciej Sobczak
  2019-04-04  7:17             ` Dmitry A. Kazakov
                               ` (2 more replies)
  2019-04-04 16:17           ` Optikos
  2 siblings, 3 replies; 146+ messages in thread
From: Maciej Sobczak @ 2019-04-04  5:44 UTC (permalink / raw)


> In none of my projects GDB works.
> 
> P.S. It never worked reliable in GPS and I bet it never will.

This is very troubling. I understand the sentiment here that Ada is so good in error prevention that debuggers are not needed at all, but what I find in projects I'm related with is that debuggers are not used for debugging anyway.

The major use for debuggers that I see is in integration testing, where test procedures expect particular values in particular variables (or even exact memory locations) in particular circumstances. The test is successful if such expectations are confirmed. Even for a presumably 100% correct program such a test has to be done if foreseen by project plans.

So, we have another paradox: Ada is so good in error prevention that the community does not care about having a proper debugger, and then the lack of working debugger prevents people from choosing Ada for projects that have rigorous integration testing culture. Part of the paradox is that such projects happen to be safety-critical, where Ada is supposed to be the preferred solution. And then they use C, where debuggers work like a charm.

Again: debuggers are not only for debugging and you better get them working right (by, well... debugging them?).

-- 
Maciej Sobczak * http://www.inspirel.com


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 21:12           ` Simon Wright
@ 2019-04-04  7:09             ` Dmitry A. Kazakov
  0 siblings, 0 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-04-04  7:09 UTC (permalink / raw)


On 2019-04-03 23:12, Simon Wright wrote:

> But 90% of the time it's a matter of looking at the fatal exception
> traceback.

Yes, that is why static exception contracts could be a great help.

In fact one could argue that Ada is weakly typed without them. Consider:

    function Foo return Integer; -- May raise Constraint_Error

This is not properly typed! The type of the result is not Integer. It is 
rather

    Integer or propagating Constraint_Error

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-04  5:44           ` Maciej Sobczak
@ 2019-04-04  7:17             ` Dmitry A. Kazakov
  2019-04-04  7:22             ` Paul Rubin
  2019-04-04 12:28             ` Simon Wright
  2 siblings, 0 replies; 146+ messages in thread
From: Dmitry A. Kazakov @ 2019-04-04  7:17 UTC (permalink / raw)


On 2019-04-04 07:44, Maciej Sobczak wrote:

> So, we have another paradox: Ada is so good in error prevention that the community does not care about having a proper debugger, and then the lack of working debugger prevents people from choosing Ada for projects that have rigorous integration testing culture. Part of the paradox is that such projects happen to be safety-critical, where Ada is supposed to be the preferred solution. And then they use C, where debuggers work like a charm.

In the Conway's game of life there are populations called "Eden garden" 
ones no other state leads to. It is not a paradox at all, that some 
things cannot emerge though natural gradual change.

> Again: debuggers are not only for debugging and you better get them working right (by, well... debugging them?).

Yes, but my guess is that AdaCore has no spare resources to invest into 
rewriting GDB. Another guess is that GDB/GNU debug info format might 
have some fundamental design issues.

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

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-04  5:44           ` Maciej Sobczak
  2019-04-04  7:17             ` Dmitry A. Kazakov
@ 2019-04-04  7:22             ` Paul Rubin
  2019-04-04  8:37               ` Niklas Holsti
  2019-04-04 12:28             ` Simon Wright
  2 siblings, 1 reply; 146+ messages in thread
From: Paul Rubin @ 2019-04-04  7:22 UTC (permalink / raw)


Maciej Sobczak <see.my.homepage@gmail.com> writes:
> The major use for debuggers that I see is in integration testing,
> where test procedures expect particular values in particular variables
> (or even exact memory locations) in particular circumstances.

You should really automate tests like that.

I find debuggers very useful for understanding how an unfamiliar piece
of poorly documented code works.  What are the conditions when this
function XYZ is called, and how does the program get there?  Load the
program into debugger, set breakpoint at XYZ, and run.  What happens in
case of this other input?  Set breakpoint earlier, run with other input
and single step to understand flow of the program, etc.

There will always be logic errors in programs too.  Sure you can debug
them with print statements and recompiles, but debuggers and breakpoints
basically give you a way to insert the print statements interactively
and dynamically while the program is running.

I managed to use gdb with Ada but I only tried it with a few simple and
small programs.  If there's trouble using it with bigger programs that's
not good and I'd hope Adacore would address it.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-04  7:22             ` Paul Rubin
@ 2019-04-04  8:37               ` Niklas Holsti
  2019-04-05  0:13                 ` Randy Brukardt
  2019-04-05  5:45                 ` Maciej Sobczak
  0 siblings, 2 replies; 146+ messages in thread
From: Niklas Holsti @ 2019-04-04  8:37 UTC (permalink / raw)


On 19-04-04 10:22 , Paul Rubin wrote:
> Maciej Sobczak <see.my.homepage@gmail.com> writes:
>> The major use for debuggers that I see is in integration testing,
>> where test procedures expect particular values in particular variables
>> (or even exact memory locations) in particular circumstances.
>
> You should really automate tests like that.

As gdb can be scripted, the tests that Maciej describes can probably be 
automated, albeit with considerable effort, especially if the scripts 
should be robust to evolution of the SW under test (changing the line 
numbers of the required breakpoints, etc.)

In my domain (on-board satellite SW) the current practice is to fuse 
unit tests with integration tests, with a relatively smooth progression 
from operation-level tests, through module-level tests, to 
subsystem-level tests, with mostly the same techniques and tools at all 
levels: provide inputs, check outputs and calls (with stubs), measure 
coverage. Debuggers are not used.

It is true that current unit-testing tools do not easily let one see and 
check internal states and values, in the way Maciej describes that gdb 
is used. However, I don't think that gdb or other current debuggers are 
ideal tools for automated checking of internal states. I have seen 
increasing activity (conferences and such) on "run-time verification", 
and I would expect better tools to emerge from those activities.

> I find debuggers very useful for understanding how an unfamiliar piece
> of poorly documented code works.  What are the conditions when this
> function XYZ is called, and how does the program get there?  Load the
> program into debugger, set breakpoint at XYZ, and run.

You see only one _instance_ of an execution. I usually prefer to have a 
static analysis give me call-graph which represents _all_ possible 
executions and gives me a general understanding of the program. But I 
agree that instances can also be useful to check that one's general 
understanding is correct.

Both points (Maciej's and Paul's) support my opinion that "debugger" is 
the wrong word for these tools. Their main use is to _view_ or _inspect_ 
the execution states of a program, not to "remove bugs".

> What happens in case of this other input?  Set breakpoint earlier,
> run with other input and single step to understand flow of the
> program, etc.

That is exactly the form of trial-and-error "debugging" that I abhor, 
because it usually provides a mass of instances from which I find it 
hard to extract any general understanding. Moreover, I find it less 
troublesome to modify the logging/tracing set-up before a re-run. The 
recompilation time is insignificant compared to the thinking time.

> There will always be logic errors in programs too.  Sure you can debug
> them with print statements and recompiles, but debuggers and breakpoints
> basically give you a way to insert the print statements interactively
> and dynamically while the program is running.

Except for real-time, concurrent programs... and with quite some 
problems to "print" complex data structures in readable form.

I do think that we should have ways, and better ways, to inspect and 
check program executions at run time.

One could say that most of the effort, so far, in programming tool 
development has been on means to let programmers define what the program 
_should_ do, with increasingly expressive and powerful programming 
languages and compilers or other means to facilitate the execution of 
the programs so defined.

But work on tools that let us see and understand what the program 
_actually_ does has lagged behind. There has been work on algorithm 
visualization, including work to visualize task switches and inter-task 
communications (scheduling traces), and much work on visualization of 
program outputs, but not much work on presenting program executions in 
understandable yet precise ways.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-04  5:44           ` Maciej Sobczak
  2019-04-04  7:17             ` Dmitry A. Kazakov
  2019-04-04  7:22             ` Paul Rubin
@ 2019-04-04 12:28             ` Simon Wright
  2 siblings, 0 replies; 146+ messages in thread
From: Simon Wright @ 2019-04-04 12:28 UTC (permalink / raw)


Maciej Sobczak <see.my.homepage@gmail.com> writes:

> Again: debuggers are not only for debugging and you better get them
> working right (by, well... debugging them?).

That can be .. extremely confusing!


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-02 21:55                         ` Randy Brukardt
@ 2019-04-04 15:07                           ` Simon Wright
  0 siblings, 0 replies; 146+ messages in thread
From: Simon Wright @ 2019-04-04 15:07 UTC (permalink / raw)


"Randy Brukardt" <randy@rrsoftware.com> writes:

> "Simon Wright" <simon@pushface.org> wrote in message 
> news:lywokdfk5q.fsf@pushface.org...
>> "Randy Brukardt" <randy@rrsoftware.com> writes:
>>
>>> The only way to make such a check that wouldn't trigger all of the
>>> time would require looking at both the body and the call at the same
>>> time -- a complete abandonment of privacy and separation of
>>> concerns.
>>
>> But it would be the compiler looking, not me.
>
> Doesn't matter. One can't depend on the contract of a subprogram if
> some calls are going to be illegal/raise P_E because of the contents
> of the body.

Sorry: I was confusing 'private' and privacy

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-03 17:15         ` Dmitry A. Kazakov
  2019-04-03 21:12           ` Simon Wright
  2019-04-04  5:44           ` Maciej Sobczak
@ 2019-04-04 16:17           ` Optikos
  2 siblings, 0 replies; 146+ messages in thread
From: Optikos @ 2019-04-04 16:17 UTC (permalink / raw)


On Wednesday, April 3, 2019 at 1:15:24 PM UTC-4, Dmitry A. Kazakov wrote:
> On 2019-04-03 18:16, Simon Wright wrote:
> > "Dmitry A. Kazakov" writes:
> > 
> >>> Which feature(s) [that other debuggers have] do you think are
> >>> missing from GDB when debugging Ada?
> >>
> >> Other debuggers work, GDB does not. If you have an Ada project of a
> >> moderate size GDB stops working.
> > 
> > How big is "moderate"?
> 
> In none of my projects GDB works. I never tried to figure out if that is
> related to the number of compilation units or number of library projects 
> involved.
> 
> When you click Debug->Initialize->your-main-program in GPS and debugger 
> does not start you know you reached the point.
> 
> P.S. It never worked reliable in GPS and I bet it never will.

Thank you, Dmitry.  That sufficiently answers my list of questions above.

I am going to assume that bringing GNAT (whose upper annotated-AST stage is written in Ada) up inside GDB would be big enough to observe the defect.

Perhaps the reason that it has never been debugged is the chain of
1) the large-sized Ada executable must be brought up in
2) a(n inner) GDB-under-test session that itself is in
3) another (outer) GDB session.

Taming this chain might require using a few more features than usual (e.g., remote debugging through pseudoterminal; attach outer-GDB to running inner-GDB-under-test via running process in /proc).


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-04  8:37               ` Niklas Holsti
@ 2019-04-05  0:13                 ` Randy Brukardt
  2019-04-05  5:45                 ` Maciej Sobczak
  1 sibling, 0 replies; 146+ messages in thread
From: Randy Brukardt @ 2019-04-05  0:13 UTC (permalink / raw)


"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:gglu1uFlu3fU1@mid.individual.net...
...
> That is exactly the form of trial-and-error "debugging" that I abhor, 
> because it usually provides a mass of instances from which I find it hard 
> to extract any general understanding. Moreover, I find it less troublesome 
> to modify the logging/tracing set-up before a re-run. The recompilation 
> time is insignificant compared to the thinking time.

On top of which, "logging" doesn't have to be a fully static, on-off 
proposition. Most of my programs have multiple levels of logging that can be 
controlled for a running program. So if a problem shows up in some area, 
turning on the logging for that area often will show enough information to 
eliminate the problem without any recompilation (well, until deploying the 
actual fix).

For instance, the Janus/Ada compiler has an extensive tracing menu that can 
be accessed with both a compiler option, and by placing a pragma in the 
problematic source code. I almost never change the compiler code 
until/unless that tracing proves insufficient. I've had to write substantial 
new tracing occassionally, but that often is a worthwhile permanent addition 
to the code. The number of times I have to write new, one-time tracing code 
is probably less than one in twenty bugs.

Using a debugger isn't very practical for Janus/Ada, because each compiler 
pass depends on the previous one, and thus one can't just run some pass of 
the compiler without a complete set of temporary files from the previous 
pass. Plus, the temporary files are named with the process id that created 
them, and of course the debugger uses a different PID. And of course a 
completed run of a pass  deletes or modifies some of the temporary files. 
There are ways around those issues, but there rarely is a problem that 
justifies going to that level. (I only recall doing it once, and that may 
have been more about testing the debugger rather than using it for an actual 
purpose.)

The other programs that I've worked on in recent years (the Claw Builder, 
the Trash-Finder spam filter, and the AdaIC web server) also would be 
difficult to run under a debugger (the first because of GUI interference, 
and the latter two because of the real-time and never-terminating nature). 
Logging/tracing has worked well in all of those.

                               Randy.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-04  8:37               ` Niklas Holsti
  2019-04-05  0:13                 ` Randy Brukardt
@ 2019-04-05  5:45                 ` Maciej Sobczak
  2019-04-05 15:17                   ` Optikos
  1 sibling, 1 reply; 146+ messages in thread
From: Maciej Sobczak @ 2019-04-05  5:45 UTC (permalink / raw)


> As gdb can be scripted, the tests that Maciej describes can probably be 
> automated,

Yes.

> albeit with considerable effort,

Not really. I would say there is no need for this effort to be higher than with any other form of test automation. Note that as with anything else in software, recurring problems can be mitigated by additional code. That is, if testing this way is difficult, then the difficulty is similar for the whole class of similar tests and as such that difficulty can be refactored away to additional utility (library/framework/etc.) with simpler (higher-level) interface.

> especially if the scripts 
> should be robust to evolution of the SW under test (changing the line 
> numbers of the required breakpoints, etc.)

This is a wider problem of traceability. You have to solve this problem anyway for the coverage analysis, for example. And the solution, whatever you happen to use (like tool-readable labels in source comments), will help with debugging, too.

In any case, yes, some projects need the debugger to test individual memory locations. The lack of proper tools is a technology risk.

> However, I don't think that gdb or other current debuggers are 
> ideal tools for automated checking of internal states.

They are not. But a non-ideal working debugger is still better than a not working one.

-- 
Maciej Sobczak * http://www.inspirel.com

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-05  5:45                 ` Maciej Sobczak
@ 2019-04-05 15:17                   ` Optikos
  2019-04-06  1:38                     ` Jere
  0 siblings, 1 reply; 146+ messages in thread
From: Optikos @ 2019-04-05 15:17 UTC (permalink / raw)


On Friday, April 5, 2019 at 1:45:20 AM UTC-4, Maciej Sobczak wrote:
> > As gdb can be scripted, the tests that Maciej describes can probably be 
> > automated,
> 
> Yes.
> 
> > albeit with considerable effort,
> 
> Not really. I would say there is no need for this effort to be higher than with any other form of test automation. Note that as with anything else in software, recurring problems can be mitigated by additional code. That is, if testing this way is difficult, then the difficulty is similar for the whole class of similar tests and as such that difficulty can be refactored away to additional utility (library/framework/etc.) with simpler (higher-level) interface.
> 
> > especially if the scripts 
> > should be robust to evolution of the SW under test (changing the line 
> > numbers of the required breakpoints, etc.)
> 
> This is a wider problem of traceability. You have to solve this problem anyway for the coverage analysis, for example. And the solution, whatever you happen to use (like tool-readable labels in source comments), will help with debugging, too.
> 
> In any case, yes, some projects need the debugger to test individual memory locations. The lack of proper tools is a technology risk.
> 
> > However, I don't think that gdb or other current debuggers are 
> > ideal tools for automated checking of internal states.
> 
> They are not. But a non-ideal working debugger is still better than a not working one.

Which features do you consider as missing in GDB regarding GNAT Ada that make GDB non-ideal?


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-05 15:17                   ` Optikos
@ 2019-04-06  1:38                     ` Jere
  2019-04-06  4:25                       ` alby.gamper
  0 siblings, 1 reply; 146+ messages in thread
From: Jere @ 2019-04-06  1:38 UTC (permalink / raw)


On Friday, April 5, 2019 at 11:17:55 AM UTC-4, Optikos wrote:
> On Friday, April 5, 2019 at 1:45:20 AM UTC-4, Maciej Sobczak wrote:
> > > As gdb can be scripted, the tests that Maciej describes can probably be 
> > > automated,
> > 
> > Yes.
> > 
> > > albeit with considerable effort,
> > 
> > Not really. I would say there is no need for this effort to be higher than with any other form of test automation. Note that as with anything else in software, recurring problems can be mitigated by additional code. That is, if testing this way is difficult, then the difficulty is similar for the whole class of similar tests and as such that difficulty can be refactored away to additional utility (library/framework/etc.) with simpler (higher-level) interface.
> > 
> > > especially if the scripts 
> > > should be robust to evolution of the SW under test (changing the line 
> > > numbers of the required breakpoints, etc.)
> > 
> > This is a wider problem of traceability. You have to solve this problem anyway for the coverage analysis, for example. And the solution, whatever you happen to use (like tool-readable labels in source comments), will help with debugging, too.
> > 
> > In any case, yes, some projects need the debugger to test individual memory locations. The lack of proper tools is a technology risk.
> > 
> > > However, I don't think that gdb or other current debuggers are 
> > > ideal tools for automated checking of internal states.
> > 
> > They are not. But a non-ideal working debugger is still better than a not working one.
> 
> Which features do you consider as missing in GDB regarding GNAT Ada that make GDB non-ideal?

I can't speak for GDB specifically, but at some point (2015 maybe?) they
redid the GUI interface in GPS to the debugger and it became completely 
unintuitive for me.  The few times I have had to debug Ada code involved
access types and manual memory management.  They used to have a really
good interface that would visually display records and fields, and when
I clicked on an access type variable, it would pop open another box with
the record that variable pointed to.  For custom containers this was really
handy for debugging.  It was a very handy and visual way to map out memory
for those rarer times I had to actually manage it.  Now I just use my
Smart_Access packages (once they fixed the GNAT bugs), though I still 
don't expose those to clients.


^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-06  1:38                     ` Jere
@ 2019-04-06  4:25                       ` alby.gamper
  2019-04-06  6:49                         ` Jere
  0 siblings, 1 reply; 146+ messages in thread
From: alby.gamper @ 2019-04-06  4:25 UTC (permalink / raw)


On Saturday, April 6, 2019 at 12:38:57 PM UTC+11, Jere wrote:
> On Friday, April 5, 2019 at 11:17:55 AM UTC-4, Optikos wrote:
> > On Friday, April 5, 2019 at 1:45:20 AM UTC-4, Maciej Sobczak wrote:
> > > > As gdb can be scripted, the tests that Maciej describes can probably be 
> > > > automated,
> > > 
> > > Yes.
> > > 
> > > > albeit with considerable effort,
> > > 
> > > Not really. I would say there is no need for this effort to be higher than with any other form of test automation. Note that as with anything else in software, recurring problems can be mitigated by additional code. That is, if testing this way is difficult, then the difficulty is similar for the whole class of similar tests and as such that difficulty can be refactored away to additional utility (library/framework/etc.) with simpler (higher-level) interface.
> > > 
> > > > especially if the scripts 
> > > > should be robust to evolution of the SW under test (changing the line 
> > > > numbers of the required breakpoints, etc.)
> > > 
> > > This is a wider problem of traceability. You have to solve this problem anyway for the coverage analysis, for example. And the solution, whatever you happen to use (like tool-readable labels in source comments), will help with debugging, too.
> > > 
> > > In any case, yes, some projects need the debugger to test individual memory locations. The lack of proper tools is a technology risk.
> > > 
> > > > However, I don't think that gdb or other current debuggers are 
> > > > ideal tools for automated checking of internal states.
> > > 
> > > They are not. But a non-ideal working debugger is still better than a not working one.
> > 
> > Which features do you consider as missing in GDB regarding GNAT Ada that make GDB non-ideal?
> 
> I can't speak for GDB specifically, but at some point (2015 maybe?) they
> redid the GUI interface in GPS to the debugger and it became completely 
> unintuitive for me.  The few times I have had to debug Ada code involved
> access types and manual memory management.  They used to have a really
> good interface that would visually display records and fields, and when
> I clicked on an access type variable, it would pop open another box with
> the record that variable pointed to.  For custom containers this was really
> handy for debugging.  It was a very handy and visual way to map out memory
> for those rarer times I had to actually manage it.  Now I just use my
> Smart_Access packages (once they fixed the GNAT bugs), though I still 
> don't expose those to clients.

Has anyone tried the debugging support in VisualAda. It supports both GDB via
the MI interface and if you opt in to use the MS linker, you can also use the
native MS debugger.

Both options support setting breakpoints, view/change symbols/variables, etc..

Note the native debugger will also present the internal symbols/variables, not
sure if this is a good or a bad thing?. 

One of the enhancements that I plan for the next release is adding some debug
visualizers for types such as strings and unbounded strings, which by default
are not presented / shown in a user friendly manner

Suggestions on other improvements are welcome

Alex

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-06  4:25                       ` alby.gamper
@ 2019-04-06  6:49                         ` Jere
  2019-04-06  8:24                           ` alby.gamper
  0 siblings, 1 reply; 146+ messages in thread
From: Jere @ 2019-04-06  6:49 UTC (permalink / raw)


On Saturday, April 6, 2019 at 12:25:48 AM UTC-4, alby....@gmail.com wrote:
> On Saturday, April 6, 2019 at 12:38:57 PM UTC+11, Jere wrote:
> > On Friday, April 5, 2019 at 11:17:55 AM UTC-4, Optikos wrote:
> > > On Friday, April 5, 2019 at 1:45:20 AM UTC-4, Maciej Sobczak wrote:
> > > > > As gdb can be scripted, the tests that Maciej describes can probably be 
> > > > > automated,
> > > > 
> > > > Yes.
> > > > 
> > > > > albeit with considerable effort,
> > > > 
> > > > Not really. I would say there is no need for this effort to be higher than with any other form of test automation. Note that as with anything else in software, recurring problems can be mitigated by additional code. That is, if testing this way is difficult, then the difficulty is similar for the whole class of similar tests and as such that difficulty can be refactored away to additional utility (library/framework/etc.) with simpler (higher-level) interface.
> > > > 
> > > > > especially if the scripts 
> > > > > should be robust to evolution of the SW under test (changing the line 
> > > > > numbers of the required breakpoints, etc.)
> > > > 
> > > > This is a wider problem of traceability. You have to solve this problem anyway for the coverage analysis, for example. And the solution, whatever you happen to use (like tool-readable labels in source comments), will help with debugging, too.
> > > > 
> > > > In any case, yes, some projects need the debugger to test individual memory locations. The lack of proper tools is a technology risk.
> > > > 
> > > > > However, I don't think that gdb or other current debuggers are 
> > > > > ideal tools for automated checking of internal states.
> > > > 
> > > > They are not. But a non-ideal working debugger is still better than a not working one.
> > > 
> > > Which features do you consider as missing in GDB regarding GNAT Ada that make GDB non-ideal?
> > 
> > I can't speak for GDB specifically, but at some point (2015 maybe?) they
> > redid the GUI interface in GPS to the debugger and it became completely 
> > unintuitive for me.  The few times I have had to debug Ada code involved
> > access types and manual memory management.  They used to have a really
> > good interface that would visually display records and fields, and when
> > I clicked on an access type variable, it would pop open another box with
> > the record that variable pointed to.  For custom containers this was really
> > handy for debugging.  It was a very handy and visual way to map out memory
> > for those rarer times I had to actually manage it.  Now I just use my
> > Smart_Access packages (once they fixed the GNAT bugs), though I still 
> > don't expose those to clients.
> 
> Has anyone tried the debugging support in VisualAda. It supports both GDB via
> the MI interface and if you opt in to use the MS linker, you can also use the
> native MS debugger.
> 
> Both options support setting breakpoints, view/change symbols/variables, etc..
> 
> Note the native debugger will also present the internal symbols/variables, not
> sure if this is a good or a bad thing?. 
> 
> One of the enhancements that I plan for the next release is adding some debug
> visualizers for types such as strings and unbounded strings, which by default
> are not presented / shown in a user friendly manner
> 
> Suggestions on other improvements are welcome
> 
> Alex

I started to try it out seriously a while back, but it required a specific 
installation path of some things and I did not have that setup the way it
wanted.  I've been meaning to take a stab at it again.  I've just been 
distracted.

^ permalink raw reply	[flat|nested] 146+ messages in thread

* Re: Intervention needed?
  2019-04-06  6:49                         ` Jere
@ 2019-04-06  8:24                           ` alby.gamper
  0 siblings, 0 replies; 146+ messages in thread
From: alby.gamper @ 2019-04-06  8:24 UTC (permalink / raw)


On Saturday, April 6, 2019 at 5:49:35 PM UTC+11, Jere wrote:
> On Saturday, April 6, 2019 at 12:25:48 AM UTC-4, alby....@gmail.com wrote:
> > On Saturday, April 6, 2019 at 12:38:57 PM UTC+11, Jere wrote:
> > > On Friday, April 5, 2019 at 11:17:55 AM UTC-4, Optikos wrote:
> > > > On Friday, April 5, 2019 at 1:45:20 AM UTC-4, Maciej Sobczak wrote:
> > > > > > As gdb can be scripted, the tests that Maciej describes can probably be 
> > > > > > automated,
> > > > > 
> > > > > Yes.
> > > > > 
> > > > > > albeit with considerable effort,
> > > > > 
> > > > > Not really. I would say there is no need for this effort to be higher than with any other form of test automation. Note that as with anything else in software, recurring problems can be mitigated by additional code. That is, if testing this way is difficult, then the difficulty is similar for the whole class of similar tests and as such that difficulty can be refactored away to additional utility (library/framework/etc.) with simpler (higher-level) interface.
> > > > > 
> > > > > > especially if the scripts 
> > > > > > should be robust to evolution of the SW under test (changing the line 
> > > > > > numbers of the required breakpoints, etc.)
> > > > > 
> > > > > This is a wider problem of traceability. You have to solve this problem anyway for the coverage analysis, for example. And the solution, whatever you happen to use (like tool-readable labels in source comments), will help with debugging, too.
> > > > > 
> > > > > In any case, yes, some projects need the debugger to test individual memory locations. The lack of proper tools is a technology risk.
> > > > > 
> > > > > > However, I don't think that gdb or other current debuggers are 
> > > > > > ideal tools for automated checking of internal states.
> > > > > 
> > > > > They are not. But a non-ideal working debugger is still better than a not working one.
> > > > 
> > > > Which features do you consider as missing in GDB regarding GNAT Ada that make GDB non-ideal?
> > > 
> > > I can't speak for GDB specifically, but at some point (2015 maybe?) they
> > > redid the GUI interface in GPS to the debugger and it became completely 
> > > unintuitive for me.  The few times I have had to debug Ada code involved
> > > access types and manual memory management.  They used to have a really
> > > good interface that would visually display records and fields, and when
> > > I clicked on an access type variable, it would pop open another box with
> > > the record that variable pointed to.  For custom containers this was really
> > > handy for debugging.  It was a very handy and visual way to map out memory
> > > for those rarer times I had to actually manage it.  Now I just use my
> > > Smart_Access packages (once they fixed the GNAT bugs), though I still 
> > > don't expose those to clients.
> > 
> > Has anyone tried the debugging support in VisualAda. It supports both GDB via
> > the MI interface and if you opt in to use the MS linker, you can also use the
> > native MS debugger.
> > 
> > Both options support setting breakpoints, view/change symbols/variables, etc..
> > 
> > Note the native debugger will also present the internal symbols/variables, not
> > sure if this is a good or a bad thing?. 
> > 
> > One of the enhancements that I plan for the next release is adding some debug
> > visualizers for types such as strings and unbounded strings, which by default
> > are not presented / shown in a user friendly manner
> > 
> > Suggestions on other improvements are welcome
> > 
> > Alex
> 
> I started to try it out seriously a while back, but it required a specific 
> installation path of some things and I did not have that setup the way it
> wanted.  I've been meaning to take a stab at it again.  I've just been 
> distracted.

Hi Jere

You may/will find that the version since 1.1.10 actually addresses the issue
that I believe you are referring to. Try the "Console Application" template
initially (which uses GNAT throughout, and GDB as a debugger) and then change
the project properties to use the MS linker

The MS linker can be set via the "Project Properties", ie right click the
project -> select "Properties" and then set "Use Microsoft Linker" within
the "General Ada" section

Happy to assist if you are having issues with Visual Studio

Alex

^ permalink raw reply	[flat|nested] 146+ messages in thread

end of thread, other threads:[~2019-04-06  8:24 UTC | newest]

Thread overview: 146+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-03-25 19:14 Intervention needed? Randy Brukardt
2019-03-25 20:44 ` Dmitry A. Kazakov
2019-03-28  0:48 ` Jere
  -- strict thread matches above, loose matches on Subject: below --
2019-04-02 22:07 Randy Brukardt
2019-04-03  7:29 ` Dmitry A. Kazakov
2019-04-03 14:31   ` Optikos
2019-04-03 14:54     ` Dmitry A. Kazakov
2019-04-03 15:29       ` Optikos
2019-04-03 16:16       ` Simon Wright
2019-04-03 17:15         ` Dmitry A. Kazakov
2019-04-03 21:12           ` Simon Wright
2019-04-04  7:09             ` Dmitry A. Kazakov
2019-04-04  5:44           ` Maciej Sobczak
2019-04-04  7:17             ` Dmitry A. Kazakov
2019-04-04  7:22             ` Paul Rubin
2019-04-04  8:37               ` Niklas Holsti
2019-04-05  0:13                 ` Randy Brukardt
2019-04-05  5:45                 ` Maciej Sobczak
2019-04-05 15:17                   ` Optikos
2019-04-06  1:38                     ` Jere
2019-04-06  4:25                       ` alby.gamper
2019-04-06  6:49                         ` Jere
2019-04-06  8:24                           ` alby.gamper
2019-04-04 12:28             ` Simon Wright
2019-04-04 16:17           ` Optikos
2019-04-03 15:07 ` Lucretia
2019-04-03 16:15   ` Simon Wright
2019-04-03 17:23 ` Niklas Holsti
2019-04-03 17:48   ` Bill Findlay
2019-04-03 21:01   ` Simon Wright
2019-04-03 18:58 ` Dennis Lee Bieber
2019-03-08 16:43 Olivier Henley
2019-03-08 16:58 ` Dmitry A. Kazakov
2019-03-08 17:31 ` gautier_niouzes
2019-03-11 14:31   ` antispam
2019-03-11 15:07     ` gautier_niouzes
2019-03-11 17:19     ` Dmitry A. Kazakov
2019-03-11 15:34 ` Lucretia
2019-03-11 17:30   ` Simon Wright
2019-03-11 17:42     ` Dmitry A. Kazakov
2019-03-11 18:14       ` AdaMagica
2019-03-11 19:52   ` Olivier Henley
2019-03-11 20:04     ` Lucretia
2019-03-11 22:08   ` Jeffrey R. Carter
2019-03-12  2:04     ` Lucretia
2019-03-12 13:17       ` Olivier Henley
2019-03-12 16:32       ` Jeffrey R. Carter
2019-03-12 16:56         ` Lucretia
2019-03-12 17:20           ` Lucretia
2019-03-12 18:14         ` Olivier Henley
2019-03-12 19:21           ` Lucretia
2019-03-12 21:53             ` Randy Brukardt
2019-03-13 10:50               ` Jere
2019-03-17 12:52               ` Optikos
2019-03-17 16:37                 ` Luke A. Guest
2019-03-17 16:48                 ` Paul Rubin
2019-03-20  0:49                   ` Optikos
2019-03-20  1:04                     ` Paul Rubin
2019-03-20  1:19                       ` Optikos
2019-03-18 23:36                 ` Randy Brukardt
2019-03-19  2:18                   ` Optikos
2019-03-19  8:44                     ` Dmitry A. Kazakov
2019-03-19  9:53                       ` Optikos
2019-03-19 22:13                         ` Randy Brukardt
2019-03-19 22:26                           ` Paul Rubin
2019-03-20  1:08                             ` Jere
2019-03-22  2:26                               ` Randy Brukardt
2019-03-23 15:56                                 ` Jeffrey R. Carter
2019-03-23 21:38                                   ` Paul Rubin
2019-03-19 22:36                           ` Optikos
2019-03-19 23:13                             ` Randy Brukardt
2019-03-20  1:28                               ` Jere
2019-03-20  8:42                                 ` Dmitry A. Kazakov
2019-03-22  2:00                                 ` Randy Brukardt
2019-03-22 11:10                                   ` Jere
2019-03-23  8:03                                     ` Randy Brukardt
2019-03-23 21:32                                       ` Jere
2019-03-20  7:59                               ` Optikos
2019-03-22  2:16                                 ` Randy Brukardt
2019-03-22  8:38                                   ` Optikos
2019-03-22 10:54                                     ` Jere
2019-03-23  7:53                                       ` Randy Brukardt
2019-03-23 13:59                                         ` Jere
2019-03-23 21:19                                           ` Jere
2019-03-23 21:29                                             ` Paul Rubin
2019-03-26  8:09                                           ` Optikos
2019-03-20  1:20                           ` Jere
2019-03-22  2:30                             ` Randy Brukardt
2019-03-22  9:08                               ` Dmitry A. Kazakov
2019-03-22 22:23                                 ` Optikos
2019-03-27 19:20                                   ` G. B.
2019-03-27 21:02                                     ` Paul Rubin
2019-03-28  7:01                                       ` Maciej Sobczak
2019-03-28  7:17                                         ` Paul Rubin
2019-03-28  8:39                                           ` Simon Wright
2019-03-30  4:31                                             ` Paul Rubin
2019-03-30 22:14                                           ` Robert A Duff
2019-03-30 22:55                                             ` Paul Rubin
2019-03-28  9:06                                         ` Dmitry A. Kazakov
2019-03-28 20:48                                           ` G. B.
2019-03-29  5:13                                             ` Bojan Bozovic
2019-03-29  8:13                                               ` Dmitry A. Kazakov
2019-03-29  6:57                                           ` Maciej Sobczak
2019-03-29  7:13                                             ` Paul Rubin
2019-03-29  8:39                                             ` Dmitry A. Kazakov
2019-04-01 15:13                                               ` Optikos
2019-04-01 16:51                                                 ` Dmitry A. Kazakov
2019-04-01 21:42                                                   ` Randy Brukardt
2019-04-02  8:30                                                     ` Dmitry A. Kazakov
2019-04-02 15:53                                                       ` Anh Vo
2019-03-19 22:04                       ` Randy Brukardt
2019-03-19 22:22                         ` Paul Rubin
2019-03-19 23:01                           ` Randy Brukardt
2019-03-19  9:37                     ` Optikos
2019-03-19 22:21                       ` Randy Brukardt
2019-03-29 17:56                   ` Florian Weimer
2019-03-29 22:17                     ` Randy Brukardt
2019-03-29 22:35                       ` Florian Weimer
2019-04-01 21:17                         ` Randy Brukardt
2019-03-29 17:41               ` Florian Weimer
2019-03-29 22:16                 ` Randy Brukardt
2019-03-29 22:43                   ` Florian Weimer
2019-04-01 21:29                     ` Randy Brukardt
2019-04-01 22:14                       ` Simon Wright
2019-04-02 21:55                         ` Randy Brukardt
2019-04-04 15:07                           ` Simon Wright
2019-03-12 21:41         ` Randy Brukardt
2019-03-13  9:10     ` Maciej Sobczak
2019-03-13 11:08       ` Jere
2019-03-13 11:11         ` Jere
2019-03-13 11:59         ` Jere
2019-03-13 13:44       ` Olivier Henley
2019-03-13 15:56         ` Simon Wright
2019-03-13 16:25           ` Olivier Henley
2019-03-14  0:40             ` Simon Wright
2019-03-13 16:27           ` Olivier Henley
2019-03-14 22:41         ` Randy Brukardt
2019-03-16 21:30           ` Olivier Henley
2019-03-29 17:38     ` Florian Weimer
2019-03-13 13:23 ` Olivier Henley
2019-03-22 11:10 ` Lucretia
2019-03-22 14:09   ` J-P. Rosen
2019-03-22 16:41   ` Jeffrey R. Carter
2019-03-22 17:29     ` Paul Rubin
2019-03-22 22:36       ` Optikos
2019-04-01  7:28 ` gautier_niouzes

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox