From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a24:6994:: with SMTP id e142-v6mr4735800itc.22.1521772669659; Thu, 22 Mar 2018 19:37:49 -0700 (PDT) X-Received: by 2002:a9d:29d2:: with SMTP id g18-v6mr1581330otd.5.1521772669494; Thu, 22 Mar 2018 19:37:49 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!xmission!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!199-v6no245049itl.0!news-out.google.com!d3-v6ni223itf.0!nntp.google.com!u184-v6no243441ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 22 Mar 2018 19:37:49 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=47.185.233.194; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 47.185.233.194 References: <9ed9edb1-3342-4644-89e8-9bcf404970ee@googlegroups.com> <26a1fe54-750c-45d7-9006-b6fecaa41176@googlegroups.com> <656fb1d7-48a4-40fd-bc80-10ba9c4ad0a4@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: Ada-Oriented GUI From: "Dan'l Miller" Injection-Date: Fri, 23 Mar 2018 02:37:49 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader02.eternal-september.org comp.lang.ada:51159 Date: 2018-03-22T19:37:49-07:00 List-Id: On Thursday, March 22, 2018 at 6:47:28 PM UTC-5, Randy Brukardt wrote: > "Dan'l Miller" wrote in message=20 > 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= =20 > >> wrote: > >> >> So it is inconsistent unless packed into single thread. No differen= ce, > >> >> 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 tha= t=20 > >> is > >> actually correct is impossible, so let's not even try. > > > >Here you seem to considering the only correct program to be one that=20 > >cavalierly > >mandates a designer-prescribed order to the arrival of UX-affecting even= ts, > >from all of the UI, the OS, the network, and the completion of long-runn= ing > >backend processing. >=20 > No, a correct program is one that can be reasoned about. And one cannot= =20 > reason about programs that contain race conditions ("unavoidable" or not)= .=20 > One has to impose some sort of structure to avoid race conditions/dead=20 > locks/live locks, lest the program be unanalyzable. And to have any chanc= e=20 > of believing a program is correct requires analysis. >=20 > > Why is such an engineering-time whim the only definition of correctness= . > > Why is an engineering-time a-priori prescriptive order of event-arrival= =20 > > more > > correct than Rx's a-posteriori meticulous categorization & marshaling o= f a > > descriptive order of event-arrival so that all the outcome orderings ca= n=20 > > be > > overtly handled properly? >=20 > 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 s= ublinear complexity that is manageable in a design (and verifiable at compi= le-time if Rx were moved to compile-time declarations to an Rx-equipped com= piler). > One has to architect the application so=20 > that there is very limited interaction between tasks, Not everything in the world is an Ada task of calculable maximum realtime e= xecution time. > ... > >I suppose you could try to suppress the release of any RxAda library fro= m > >now until the end of time to keep humanity safe from the reactive scourg= e > >of introducing a form of data-flow processing to Ada. That would be one > >strategy to make life worth living, I suppose. >=20 > The presence of one more library that no one much uses isn't going to bot= her=20 > me much. :-) By the 2020s (the target marketstpace for Ada2020), Rx won't be in mere lib= raries. Rx will have been moved to compile-time declarations of the datafl= ows so that they can be checked for completeness to assure that no categori= zation is incomplete. > But I've spent my entire life attempting to bring correctness to=20 > programming, with the ultimate (unachievable) goal of a compiler/language= =20 > system that detects/prevents all possible bugs from ever going undetected= in=20 > 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 categorizat= ion 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 langua= ges at compile-time. > ... I've been working on=20 > Janus/Ada infrastructure improvements without even trying to find the cod= e=20 > that needs to be modified -- the compiler/run-time tells me where changes= =20 > are needed far quicker than trying to look for them by hand. (One has to= =20 > design their code to enable this sort of thing in the first place, but th= at=20 > 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 h= aving a conversation with the compiler. > One of the goals of Ada 2020 is to bring that level of reliability to=20 > parallel programming. That means the compiler has to (conservatively)=20 > 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, b= ut outside your visibility. Arrival of a packet over a network. Completio= n of long-running batch operation. The requested async filesystem read jus= t arrived. Ooops, your virtual machine was migrated between data-centers i= n the cloud, and while you were dormant all sorts of once-pending events ar= rived & finished all higgly piggly as no longer pending, including some rar= e timeouts that need to be retried only in this bizarre data-center-migrati= on situation. The compiler's omniscience can never be omniscient enough to= see all event dependencies outside a program. Hence, the Ada2020-complian= t compiler will be provably correct for a minority subset of events contain= ed only in the small world of Ada source code and completely blind to a maj= ority of the real-world events arriving from outside Ada source code. > A system that decides to just ignore race conditions as "unavoidable" is= =20 > going in the wrong direction. Most likely, it will kill us all when it's= =20 > 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 combi= natorial explosion of this-before-that and that-before-this uncontrollable = arrival times of real-world events to conflate it to, say, linear or sublin= ear growth instead of the natural exponential-growth combinatorial explosio= n is a system whose excessively myopic compile-time mathematical proofs are= based on the wrong axiom system and the wrong possible-world in modal logi= c.