comp.lang.ada
 help / color / mirror / Atom feed
From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: Ada-Oriented GUI
Date: Fri, 23 Mar 2018 17:42:26 -0500
Date: 2018-03-23T17:42:26-05:00	[thread overview]
Message-ID: <p93vsi$e3b$1@franka.jacob-sparre.dk> (raw)
In-Reply-To: a913d10c-7799-4ec3-9357-d94e9da2deb7@googlegroups.com

"Dan'l Miller" <optikos@verizon.net> wrote in message 
news:a913d10c-7799-4ec3-9357-d94e9da2deb7@googlegroups.com...
On Thursday, March 22, 2018 at 6:47:28 PM UTC-5, Randy Brukardt wrote:
> "Dan'l Miller" wrote in message
> news:656fb1d7-48a4-40fd-bc80-10ba9c4ad0a4@googlegroups.com...
...
>> > Why is such an engineering-time whim the only definition of 
>> > correctness.
>> > Why is an engineering-time a-priori prescriptive order of event-arrival 
>> > more
>> > correct than Rx's a-posteriori meticulous categorization & marshaling 
>> > of a
>> > descriptive order of event-arrival so that all the outcome orderings 
>> > can be
>> > overtly handled properly?
>>
>> I have no idea what this even means.
>
>Then you should study up on Rx, especially from the more-academic research
>origins.  Rx is trying to teach something regarding completely 
>inventorying,
>categorizing, and mapping/folding/conflating the otherwise combinatorial
>explosion of different event-arrival orderings to instead be of linear or
>sublinear complexity that is manageable in a design (and verifiable at
>compile-time if Rx were moved to compile-time declarations to an
>Rx-equipped compiler).

A complete waste of time to stidy the jargon de-jour. Most of these things 
fade away without a trace in a couple of years. And the "problem" is 
self-inflicted - if you model anything as "events", you are already lost, 
regardless of how one implements that.

Microsoft in particular invents and releases some totally new technology 
every year or two. Most ends up with no traction whatsoever. I learned to 
stop caring because otherwise trying to keep up would drive one insane (and 
also prevent actually accomplishing anyway -- I've always figured that was 
one of Microsoft's main goals with developers, as it explains most of the 
things that they do from Solitare to changing the GUI every year.)

Moreover, I am not much interested in purely academic ideas. Particularly 
about programming, since the majority of it will be gone in a decade or so 
anyway. (Luckily, that corresponds with my official retirement date...). I'm 
mostly interested in the part that requires correctness, and that part has 
little to do with "events".

>> One has to architect the application so
>> that there is very limited interaction between tasks,
>
>Not everything in the world is an Ada task of calculable maximum realtime 
>execution time.

??? I've never once used an Ada task with "maximum realtime execution time". 
That's part of the problem using any parallel execution, IMHO

>> ...
>> >I suppose you could try to suppress the release of any RxAda library 
>> >from
>> >now until the end of time to keep humanity safe from the reactive 
>> >scourge
>> >of introducing a form of data-flow processing to Ada.  That would be one
>> >strategy to make life worth living, I suppose.
>>
>> The presence of one more library that no one much uses isn't going to 
>> bother
>> me much. :-)
>
>By the 2020s (the target marketstpace for Ada2020), Rx won't be in mere
>libraries. ...

Most likely, it will have completely disappeared. ;-)

>Rx will have been moved to compile-time declarations of the dataflows so
>that they can be checked for completeness to assure that no categorization
>is incomplete.

Ada is not the language for that, regardless of whether it works in some 
scheme, just like Ada is not the language for functional programming, even 
if you sort of can fake it for some purposes. Use a language better 
targetted to those weird special cases. Better yet, don't use any language 
at all, since most programming will be gone by then anyway. (I'm becoming 
convinced that Ada as it stands is not going to be able to appropriately 
support safe parallel programming, so we may very well be at the end of the 
lifespan of Ada anyway.)

>> But I've spent my entire life attempting to bring correctness to
>> programming, with the ultimate (unachievable) goal of a compiler/language
>> system that detects/prevents all possible bugs from ever going undetected 
>> in
>> a fielded system.
>
>  Then move Rx to compile-time declarations instead.  Just as in omitting a 
> case
>can be detected for enumerations at compile-time, omitted categorization of 
>an
>unhandled order of arrival can conceivably be detected at compile-time if 
>the
>declarations were known to an Rx-equipped compiler at compile-time. 
>Today's
>Rx is merely a prototype of what is to come in future languages at 
>compile-time.

I'm not talking about "omitting cases", something Ada has always been able 
to do very well at compile-time. Just use an appropriate enumeration. Most 
of the stuff that has come later really does not help for that (like OOP). 
The academics made such a complaint about needing to update case statements, 
but turning the declarations 90 degrees fixes nothing -- now you need to 
implement interminable overridings instead. It obviously depends on the 
problem as to whether the case statements or the overridings are bigger --  
in my programs, the overridings were much worse to deal with than updating 
the case statements.

Correctness is about verifying (preferably at compile-time) constraints and 
invariants -- on data, code, and anything else around. That is, finding bugs 
before they happen. Flow is part of that, but only a relatively small part. 
And of course, making all of those checks statically is the holy grail.


>> One of the goals of Ada 2020 is to bring that level of reliability to
>> parallel programming. That means the compiler has to (conservatively)
>> diagnose and reject data races between separately executed code.
>
>How will the ARG assure itself that it is not on a fool's errand?

We can't; that's a topic of discussion. For me personally, if we can't do 
this, then Ada is dead and I will want to be dead - there is no future in 
such a world.

>There is always at least one more origin of events outside not only your 
>control, but
>outside your visibility.  Arrival of a packet over a network.  Completion 
>of
>long-running batch operation.  The requested async filesystem read just 
>arrived.
>Ooops, your virtual machine was migrated between data-centers in the cloud, 
>and
>while you were dormant all sorts of once-pending events arrived & finished 
>all
>higgly piggly as no longer pending, including some rare timeouts that need 
>to be
>retried only in this bizarre data-center-migration situation.

If such events (that you're not interested in) aren't isolated from your 
application by the kernel, then you have a very bad architecture. And a 
massive security problem. Such an architecture has no real future unless ATT 
etc convince the public that there is no value to security and privacy. (See 
"I'd rather be dead", above.)

If they are isolated, who cares what they do? If the application depends 
upon them, then of course the compiler knows about them in the sense that 
they are handled.

>The compiler's omniscience can never be omniscient enough to see all event
>dependencies outside a program.

Why would we care about anything that happens outside of a program? One 
assumes that the virtualization and isolation of the kernel actually work. 
:-)

>Hence, the Ada2020-compliant compiler will be provably correct for a
>minority subset of events contained only in the small world of Ada source
>code and completely blind to a majority of the real-world events arriving
>from outside Ada source code.

The majority of irrelevant events. And if those events have any effect 
whatsoever on the running program (other than timing), there's a major 
archtectual problem. Besides, if you really care, you'll write the entire 
system in Ada -- Ada itself makes a fine kernel -- and then there are no 
other events even possible.

> A system that decides to just ignore race conditions as "unavoidable" is
> going in the wrong direction. Most likely, it will kill us all when it's
> running self-driving cars and autopilots.

An entirely a-priori system that fails to a-posteriori-ly overtly inventory, 
categorize, and map/fold (i.e., prune/conflate the branches of) the 
combinatorial explosion of this-before-that and that-before-this 
uncontrollable arrival times of real-world events to conflate it to, say, 
linear or sublinear growth instead of the natural exponential-growth 
combinatorial explosion is a system whose excessively myopic compile-time 
mathematical proofs are based on the wrong axiom system and the wrong 
possible-world in modal logic. 


  reply	other threads:[~2018-03-23 22:42 UTC|newest]

Thread overview: 102+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-03-18 13:33 Ada-Oriented GUI Jeffrey R. Carter
2018-03-19  2:03 ` Dan'l Miller
2018-03-19 14:10   ` Dan'l Miller
2018-03-21  9:49     ` Alejandro R. Mosteo
2018-03-21 13:58       ` Dan'l Miller
2018-03-21 18:43         ` briot.emmanuel
2018-03-21 19:17           ` Shark8
2018-03-21 22:40             ` Randy Brukardt
2018-03-21 23:52               ` Shark8
2018-03-22  6:50                 ` briot.emmanuel
2018-03-22 16:56                   ` Shark8
2018-03-23 16:29               ` Shark8
2018-03-23 22:59                 ` Randy Brukardt
2018-03-23 23:43                   ` Mehdi Saada
2018-03-26 22:09                     ` Randy Brukardt
2018-03-27  7:27                       ` Dmitry A. Kazakov
2018-03-27 23:58                         ` Randy Brukardt
2018-03-28  7:09                           ` Dmitry A. Kazakov
2018-03-22 17:34         ` Alejandro R. Mosteo
2018-03-22 17:50           ` Dan'l Miller
2018-03-22 18:58             ` Shark8
2018-03-23 12:06             ` Alejandro R. Mosteo
2018-03-20 16:41 ` Dan'l Miller
2018-03-20 21:34   ` Randy Brukardt
2018-03-21  2:22     ` Dan'l Miller
2018-03-21 21:50       ` Randy Brukardt
2018-03-22  8:45         ` Dmitry A. Kazakov
2018-03-22 10:58         ` Bojan Bozovic
2018-03-22 11:03           ` Bojan Bozovic
2018-03-21  8:25 ` Dmitry A. Kazakov
2018-03-21 14:30   ` Dan'l Miller
2018-03-21 15:57     ` vincent.diemunsch
2018-03-21 17:33       ` Dan'l Miller
2018-03-21 16:27     ` Dmitry A. Kazakov
2018-03-21 17:04       ` Dan'l Miller
2018-03-21 17:42         ` Dmitry A. Kazakov
2018-03-21 18:19           ` Dan'l Miller
2018-03-21 19:11             ` Simon Wright
2018-03-21 19:51               ` Dan'l Miller
2018-03-21 20:11                 ` Dmitry A. Kazakov
2018-03-21 20:33                   ` Dan'l Miller
2018-03-21 22:16                   ` Dan'l Miller
2018-03-22  9:12                     ` Dmitry A. Kazakov
2018-03-22 14:57                       ` Dan'l Miller
2018-03-22 15:46                         ` Bojan Bozovic
2018-03-22 14:00                     ` Dan'l Miller
2018-03-22 17:29                   ` Alejandro R. Mosteo
2018-03-21 21:58             ` Randy Brukardt
2018-03-26 21:20               ` G. B.
2018-03-21 22:33             ` Randy Brukardt
2018-03-22  1:43               ` Dan'l Miller
2018-03-22 23:47                 ` Randy Brukardt
2018-03-23  2:37                   ` Dan'l Miller
2018-03-23 22:42                     ` Randy Brukardt [this message]
2018-03-24  7:47                       ` Simon Wright
2018-03-23  9:05                   ` Jeffrey R. Carter
2018-03-23  9:48                     ` Bojan Bozovic
2018-03-23 10:20                     ` Alejandro R. Mosteo
2018-03-27 18:32                     ` Killing software and certification (was: Ada-Oriented GUI) Alejandro R. Mosteo
2018-03-27 19:25                       ` Killing software and certification Dmitry A. Kazakov
2018-03-28 13:54                         ` Alejandro R. Mosteo
2018-03-28 14:23                           ` Dmitry A. Kazakov
2018-03-28 17:06                             ` Alejandro R. Mosteo
2018-03-28 19:35                               ` Dmitry A. Kazakov
2018-03-28 15:47                           ` Jeffrey R. Carter
2018-03-28 17:02                             ` Dennis Lee Bieber
2018-03-28 17:59                             ` Dan'l Miller
2018-03-27 19:41                       ` Killing software and certification (was: Ada-Oriented GUI) Dan'l Miller
2018-03-28  0:04                         ` Randy Brukardt
2018-03-28  2:27                           ` Dan'l Miller
2018-03-28 13:54                           ` Killing software and certification Alejandro R. Mosteo
2018-03-28  0:21                       ` Killing software and certification (was: Ada-Oriented GUI) Jere
2018-03-28 13:54                         ` Killing software and certification Alejandro R. Mosteo
2018-03-23 12:31                   ` Ada-Oriented GUI Alejandro R. Mosteo
2018-03-23 12:59                     ` Dmitry A. Kazakov
2018-03-23 16:16                       ` Dan'l Miller
2018-03-23 17:18                         ` Dmitry A. Kazakov
2018-03-23 18:31                           ` Dan'l Miller
2018-03-23 20:06                             ` Dmitry A. Kazakov
2018-03-23 20:48                               ` Mehdi Saada
2018-03-23 21:18                                 ` Dmitry A. Kazakov
2018-03-24 11:36                       ` Alejandro R. Mosteo
2018-03-24 13:12                         ` Dmitry A. Kazakov
2018-03-28 14:09                           ` Alejandro R. Mosteo
2018-03-28 15:02                             ` Dmitry A. Kazakov
2018-03-28 18:07                               ` Alejandro R. Mosteo
2018-03-29  7:58                                 ` Dmitry A. Kazakov
2018-04-02 22:13                               ` Robert I. Eachus
2018-04-03  8:31                                 ` Dmitry A. Kazakov
2018-04-03 22:32                                   ` Robert I. Eachus
2018-04-04  7:30                                     ` Dmitry A. Kazakov
2018-03-25 12:57                         ` Jeffrey R. Carter
2018-03-24 16:33                   ` Dan'l Miller
2018-03-26 22:29                     ` Randy Brukardt
2018-03-27  0:15                       ` Dan'l Miller
2018-03-27  6:08                       ` Dennis Lee Bieber
2018-03-27  7:52                         ` Simon Wright
2018-03-27 14:48                           ` Dennis Lee Bieber
2018-04-01 17:37                       ` Robert I. Eachus
2018-03-25 19:19 ` Andrew Shvets
  -- strict thread matches above, loose matches on Subject: below --
2018-03-23 22:48 Randy Brukardt
2018-03-24  7:51 ` Simon Wright
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox