From: "Dan'l Miller" <optikos@verizon.net>
Subject: Re: Ada-Oriented GUI
Date: Thu, 22 Mar 2018 19:37:49 -0700 (PDT)
Date: 2018-03-22T19:37:49-07:00 [thread overview]
Message-ID: <a913d10c-7799-4ec3-9357-d94e9da2deb7@googlegroups.com> (raw)
In-Reply-To: <p91fae$3fs$1@franka.jacob-sparre.dk>
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...
> On Wednesday, March 21, 2018 at 5:33:43 PM UTC-5, Randy Brukardt wrote:
> >> "Dan'l Miller" wrote in message
> >> news:26a1fe54-750c-45d7-9006-b6fecaa41176@googlegroups.com...
> >> On Wednesday, March 21, 2018 at 12:43:04 PM UTC-5, Dmitry A. Kazakov
> >> wrote:
> >> >> So it is inconsistent unless packed into single thread. No difference,
> >> >> exiting GUI do just same.
> >>
> >> >Well, more power to you then, because you can show all those Rx folks
> >> >where their entire worldview is horribly wrong from the git-go.
> >>
> >> Obviously. :-) Their worldview appears to be that writing software that
> >> is
> >> actually correct is impossible, so let's not even try.
> >
> >Here you seem to considering the only correct program to be one that
> >cavalierly
> >mandates a designer-prescribed order to the arrival of UX-affecting events,
> >from all of the UI, the OS, the network, and the completion of long-running
> >backend processing.
>
> No, a correct program is one that can be reasoned about. And one cannot
> reason about programs that contain race conditions ("unavoidable" or not).
> One has to impose some sort of structure to avoid race conditions/dead
> locks/live locks, lest the program be unanalyzable. And to have any chance
> of believing a program is correct requires analysis.
>
> > 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).
> 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 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. 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.
> 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've been working on
> Janus/Ada infrastructure improvements without even trying to find the code
> that needs to be modified -- the compiler/run-time tells me where changes
> are needed far quicker than trying to look for them by hand. (One has to
> design their code to enable this sort of thing in the first place, but that
> pays off many times if the program has any sort of lifetime.)
Hear hear! I have been doing that myself for nearly 20 years. I call it having a conversation with the compiler.
> 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? 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. The compiler's omniscience can never be omniscient enough to see all event dependencies outside a program. 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.
> 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.
next prev parent reply other threads:[~2018-03-23 2:37 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 [this message]
2018-03-23 22:42 ` Randy Brukardt
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