Re: Ada-Oriented GUI

[Bojan Bozovic <bozovic.bojan@gmail.com>]

On Thursday, March 22, 2018 at 11:58:12 AM UTC+1, Bojan Bozovic wrote:
> On Wednesday, March 21, 2018 at 10:51:01 PM UTC+1, Randy Brukardt wrote:
> > "Dan'l Miller" <optikos@verizon.net> wrote in message 
> > news:0a1e0664-f657-4596-9672-5440ebe4caf2@googlegroups.com...
> > ...
> > >I never said that it wouldn't be.  I was saying that rarely is a design
> > >tied to absolutely running nontrivial amounts of non-UI code on the Main 
> > >thread.
> > 
> > Conventional sequential programs ran all of their code (UI and otherwise) on 
> > a single thread.
> > 
> > Requiring the program to be executed around the GUI forces anything 
> > substantial into tasks (threads), with all of the problems that entails 
> > (deadlock/livelock/data races/nondeterminism/required synchronization). 
> > Since Ada already defines the purpose and definition of the environment task 
> > (what you're calling the main thread), requiring using it for the GUI forced 
> > the entire program to be used by the GUI. And the GUI is necessarily a tiny 
> > part of any program that Ada is very appropriate for (that is, programs that 
> > need to be close to the metal and/or verifiable - a GUI itself being neither 
> > of these).
> > 
> > The problem with Claw was that it implicitly dragged those tasking issues 
> > into even sequential programs. Insisting on the GUI being primary makes 
> > those problems even worse. I'd like to see a design where the GUI was truly 
> > secondary (I couldn't figure it out, and I'm done caring personally).
> > 
> >                    Randy.
> 
> But I can imagine cases where gui would need to be verified, together with the OS itself, banking applications and applications used in hospitals to queue patient records come to mind. You're absolutely correct that applications shouldn't be designed around gui, but gui agnostic, but its all in vain if the OS itself isn't verified and nobody will bother (here's an idea, make one verified - as much as possible - posix/unix system for general use, market real time version to embedded developers which traditionally use Ada commercially, verified to DO-178C, ISO 26262 and other standards for automation, transportation and industrial use, use drivers that aren't verified from Linux or some *BSD for general use and have verified drivers for boards used in safety critical domains. There is also a problem with formal methods not being integrated in the language itself, so it's programming in Z or B with tools that generate Ada or C source, where, ideally, such intermediate steps needn't be taken. Whether programmer would use formal methods in a language or not it would depend on actual needs of a project. I havent (yet) read the book on Alphard by Shaw, Wulf and London, but they had that idea to have code verification in a language itself which could be paired with modern theorem provers. In my ideal world there wouldn't be any bugs in code, as the damage done by buggy code and hackers exploiting is enormous already. Verification would make hacking obsolete.

Not queue but handle. English is a distant second language to me, and I hope you will forgive my error.