More reliable compilers (of some programming langauges) than GNAT

More reliable compilers (of some programming langauges) than GNAT

[Victor Porton]

Ada is good.

But I have caught a few GNAT bugs while writing my software. It is too bad.

Would you recommend me another language (not Ada) which has a quality free 
compiler?

I need linking with C (like Ada Convention=>C), threads, containers library, 
and if possible reliability.

Maybe should I switch to C++? Is C++ compiler more reliable than GNAT?

I also heard of D and Swift. Huh?

Java?

Or (oh, oh, oh) plain C?

-- 
Victor Porton - http://portonvictor.org

Re: More reliable compilers (of some programming langauges) than GNAT

[AdaMagica]

Am Dienstag, 21. November 2017 16:07:47 UTC+1 schrieb Victor Porton:
> Ada is good.
> 
> But I have caught a few GNAT bugs while writing my software. It is too bad.
> 
> Would you recommend me another language (not Ada) which has a quality free 
> compiler?

compilers free of quality should be abundant for languages galore.

> I need linking with C (like Ada Convention=>C), threads, containers library, 
> and if possible reliability.
> 
> Maybe should I switch to C++? Is C++ compiler more reliable than GNAT?
> 
> I also heard of D and Swift. Huh?
> 
> Java?
> 
> Or (oh, oh, oh) plain C?
> 
> -- 
> Victor Porton - http://portonvictor.org

Re: More reliable compilers (of some programming langauges) than GNAT

[Victor Porton]

AdaMagica wrote:

> Am Dienstag, 21. November 2017 16:07:47 UTC+1 schrieb Victor Porton:
>> Ada is good.
>> 
>> But I have caught a few GNAT bugs while writing my software. It is too
>> bad.
>> 
>> Would you recommend me another language (not Ada) which has a quality
>> free compiler?
> 
> compilers free of quality should be abundant for languages galore.

What

"free of quality"?

or maybe you meant "free and quality"?

What did you mean?

>> I need linking with C (like Ada Convention=>C), threads, containers
>> library, and if possible reliability.
>> 
>> Maybe should I switch to C++? Is C++ compiler more reliable than GNAT?
>> 
>> I also heard of D and Swift. Huh?
>> 
>> Java?
>> 
>> Or (oh, oh, oh) plain C?
>> 
>> --
>> Victor Porton - http://portonvictor.org
-- 
Victor Porton - http://portonvictor.org

Re: More reliable compilers (of some programming langauges) than GNAT

[AdaMagica]

Am Dienstag, 21. November 2017 16:41:00 UTC+1 schrieb Victor Porton:
> >> a quality free compiler?

Didn't you write this? (Sorry, couldn't resist;-)

Re: More reliable compilers (of some programming langauges) than GNAT

[AdaMagica]

Am Dienstag, 21. November 2017 16:07:47 UTC+1 schrieb Victor Porton:
> Ada is good.
> 
> But I have caught a few GNAT bugs while writing my software. It is too bad.
> 
> Would you recommend me another language (not Ada) which has a quality free 
> compiler?

Now seriously:

Gnat is a very good compiler, I used it for a real time full scale flight simulator for helicopters. Yes, I stepped over compiler problems. We had an AdaCore contract, and in most cases I got a workaround within a few hours or, if needed, a wavefront in one day.

I'd never give up Ada because of a compiler with some bugs. You certainly will find workarounds.

Re: More reliable compilers (of some programming langauges) than GNAT

[Victor Porton]

AdaMagica wrote:

> Am Dienstag, 21. November 2017 16:07:47 UTC+1 schrieb Victor Porton:
>> Ada is good.
>> 
>> But I have caught a few GNAT bugs while writing my software. It is too
>> bad.
>> 
>> Would you recommend me another language (not Ada) which has a quality
>> free compiler?
> 
> Now seriously:
> 
> Gnat is a very good compiler, I used it for a real time full scale flight
> simulator for helicopters. Yes, I stepped over compiler problems. We had
> an AdaCore contract, and in most cases I got a workaround within a few
> hours or, if needed, a wavefront in one day.

I work in a nonprofit, I cannot afford GNAT PRO.

I wrote to AdaCore asking a free license for my nonprofit, but they didn't 
give.

> I'd never give up Ada because of a compiler with some bugs. You certainly
> will find workarounds.
-- 
Victor Porton - http://portonvictor.org

Re: More reliable compilers (of some programming langauges) than GNAT

[Dmitry A. Kazakov]

On 2017-11-21 17:17, Victor Porton wrote:
> AdaMagica wrote:
> 
> I work in a nonprofit, I cannot afford GNAT PRO.
> 
> I wrote to AdaCore asking a free license for my nonprofit, but they didn't
> give.
> 
>> I'd never give up Ada because of a compiler with some bugs. You certainly
>> will find workarounds.

Exactly. Work around the problem. It is possible, I do it constantly 
because GNAT always has bugs in generics and will probably ever have.

But the rest is incredibly stable.

Then compared to GCC I permanently have issues with libraries in C. Not 
one of them can be used after an update. Presently I am fighting with 
OpenSSL. Nothing is ever compatible. C++ libraries are far worse, they 
are simply impossible to maintain. Look at the list of packages in any 
Linux system and see how many versions of Python they have etc.

Ada is the most maintainable language ever and any issues GNAT might 
have is nothing compared to other languages.

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

Re: More reliable compilers (of some programming langauges) than GNAT

[Randy Brukardt]

"AdaMagica" <christ-usch.grein@t-online.de> wrote in message 
news:2fca0f38-833e-485d-9a38-febcdd507bb1@googlegroups.com...
> Am Dienstag, 21. November 2017 16:07:47 UTC+1 schrieb Victor Porton:
...
>> Would you recommend me another language (not Ada) which has a quality 
>> free
>> compiler?
>
> compilers free of quality should be abundant for languages galore.

LoL. I think the smily face is missing here. :-)

Seriously, though, the idea of a bug-free compiler for any non-trivial 
programming language is rather laughable.

It's possible that the application of proof tools to compilers will improve 
their quality (especially possible in the back-ends), but there is always 
going to be the problem of adequately expressing the correct result. One 
would have to have a completely formal description of the programming 
language -- but then how would one prove that there are no bugs in that 
formal description (most likely written in a language that hardly anyone 
would understand)? You have a problem that essentially is an infinite 
regress - you're always going to end up at some point with a description 
that cannot be proved correct (and is too complex to ensure correct).

(Note: There was a formal description and set of proofs for part of the Ada 
95 definition; supposedly, it proved that there was no problems with the 
visibility description of Ada 95; in particular that there were no 
Beaujolais effects. But no one other than the authors understood it and 
nothing further was ever done with it so far as I know.)

                                                      Randy.

Re: More reliable compilers (of some programming langauges) than GNAT

[Randy Brukardt]

"AdaMagica" <christ-usch.grein@t-online.de> wrote in message 
news:ee3bd2ac-3c7c-46a8-959f-753e8db7cdd2@googlegroups.com...
> Am Dienstag, 21. November 2017 16:41:00 UTC+1 schrieb Victor Porton:
>> >> a quality free compiler?
>
> Didn't you write this? (Sorry, couldn't resist;-)

Perhaps it isn't obvious to a non-native English speaker, but "quality free 
compiler" reads as "a compiler free of any quality" (or "a compiler without 
any quality"). As Christoph joked, it isn't the least bit hard to find any 
such compiler (although I would argue that that doesn't apply to any Ada 
compilers, you'd probably have to look at C or some other language for such 
a compiler :-).

You probably meant a "quality compiler that is free". I'd recommend GNAT for 
that, as I don't think there is any likelyhood of finding a compiler for any 
useful programing language that is better.

                                               Randy.


                                       Randy.

Re: More reliable compilers (of some programming langauges) than GNAT

[Randy Brukardt]

I said:
...
> Perhaps it isn't obvious to a non-native English speaker, but "quality 
> free compiler" reads as "a compiler free of any quality" (or "a compiler 
> without any quality"). As Christoph joked, it isn't the least bit hard to 
> find any such compiler (although I would argue that that doesn't apply to 
> any Ada compilers, you'd probably have to look at C or some other language 
> for such a compiler :-).

BTW, one reason for this is that there is a freely available independent 
test suite for Ada (the ACATS), so it is highly unlikely to see an Ada 
compiler that can't process some basic construct. So far as I'm aware, all 
Ada vendors use the ACATS as part of their standard QA, so basic bugs do not 
get into circulation. Most other languages do not have such a test suite, so 
both the commonality and the correctness of implementations is much more 
dependent on the vendor.

                                            Randy.

Re: More reliable compilers (of some programming langauges) than GNAT

[Paul Rubin]

"Randy Brukardt" <randy@rrsoftware.com> writes:
> It's possible that the application of proof tools to compilers will improve 
> their quality (especially possible in the back-ends), but there is always 
> going to be the problem of adequately expressing the correct result. 

You might like this:

    https://blog.regehr.org/archives/249

    ... I expected that we would find some flaws in CompCert’s
    formalisms. My meager experience in formal specification is that getting
    a large specification right is heroically difficult — perhaps not much
    easier than getting a complicated software system right in the first
    place. So far, however, we have found no errors in the CompCert PowerPC
    specification, their C-light specification, or in their proof
    strategy. This is pretty amazing and my opinion of the job done by the
    CompCert team is astronomically high.

It's an old article but they did in fact find some CompCert bugs back then.

Re: More reliable compilers (of some programming langauges) than GNAT

[Victor Porton]

Randy Brukardt wrote:

> I said:
> ...
>> Perhaps it isn't obvious to a non-native English speaker, but "quality
>> free compiler" reads as "a compiler free of any quality" (or "a compiler
>> without any quality"). As Christoph joked, it isn't the least bit hard to
>> find any such compiler (although I would argue that that doesn't apply to
>> any Ada compilers, you'd probably have to look at C or some other
>> language for such a compiler :-).
> 
> BTW, one reason for this is that there is a freely available independent
> test suite for Ada (the ACATS), so it is highly unlikely to see an Ada
> compiler that can't process some basic construct. So far as I'm aware, all

See
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=83027#c17
for such a bug (recently found by me, about shared libraries).

> Ada vendors use the ACATS as part of their standard QA, so basic bugs do
> not get into circulation. Most other languages do not have such a test
> suite, so both the commonality and the correctness of implementations is
> much more dependent on the vendor.
> 
>                                             Randy.
-- 
Victor Porton - http://portonvictor.org

Re: More reliable compilers (of some programming langauges) than GNAT

[Simon Wright]

Victor Porton <porton@narod.ru> writes:

> Randy Brukardt wrote:

>> BTW, one reason for this is that there is a freely available independent
>> test suite for Ada (the ACATS), so it is highly unlikely to see an Ada
>> compiler that can't process some basic construct. So far as I'm aware, all
>
> See
> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=83027#c17
> for such a bug (recently found by me, about shared libraries).

As I noted there, this problem doesn't occur on macOS or debian
jessie.

Re: More reliable compilers (of some programming langauges) than GNAT

[J-P. Rosen]

Le 22/11/2017 à 02:19, Randy Brukardt a écrit :
> Note: There was a formal description and set of proofs for part of the Ada 
> 95 definition
And of course, there was a formal definition of Ada 83 by Véronique
Donzeau-Gouge.

-- 
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

Re: More reliable compilers (of some programming langauges) than GNAT

[Randy Brukardt]

"Victor Porton" <porton@narod.ru> wrote in message 
news:ov3t3c$uvn$1@gioia.aioe.org...
> Randy Brukardt wrote:
...
>> BTW, one reason for this is that there is a freely available independent
>> test suite for Ada (the ACATS), so it is highly unlikely to see an Ada
>> compiler that can't process some basic construct. So far as I'm aware, 
>> all
>
> See
> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=83027#c17
> for such a bug (recently found by me, about shared libraries).

A "shared library" is not a "basic construct"; indeed, it is not an Ada 
construct at all so of course it has nothing to do with the quality of the 
*Ada* compiler. Indeed, many Ada compilers don't bother to support "shared 
libraries" as they are a rather useless construct that mainly serves to 
introduce bugs (if the shared library gets updated out of sync with the rest 
of the program).

                                        Randy.

Re: More reliable compilers (of some programming langauges) than GNAT

[Robert Eachus]

On Tuesday, November 21, 2017 at 8:19:28 PM UTC-5, Randy Brukardt wrote:
 
> Seriously, though, the idea of a bug-free compiler for any non-trivial 
> programming language is rather laughable.
> 
> It's possible that the application of proof tools to compilers will improve 
> their quality (especially possible in the back-ends), but there is always 
> going to be the problem of adequately expressing the correct result. One 
> would have to have a completely formal description of the programming 
> language -- but then how would one prove that there are no bugs in that 
> formal description (most likely written in a language that hardly anyone 
> would understand)? You have a problem that essentially is an infinite 
> regress - you're always going to end up at some point with a description 
> that cannot be proved correct (and is too complex to ensure correct).

I'm going to be the grinch here and invite Gödel to the party. The name GNAT was chosen as a subtle reference to the fact that no compiler can be proven to completely and correctly implement the definition of the programming language. (For sufficiently complex programming languages but that bar is very, very low.*)  So Gnat has always been known to have at least one bug in it.  Yes, it is possible to write provably correct programs in Ada.  (You may want to look at the difference between primitive recursive functions and partial recursive functions in a textbook on theory of computation, or analysis of algorithms.)

The problem is that for some recursive functions, it is not possible to prove that the input to the compiler (in Ada) and the output (in machine language) compute the same function for some partially recursive functions. A corollary of this, is that there must be programs for which the compiler output is incorrect.  Otherwise the compiler would constitute an (impossible) proof of correctness.  Or, the compiler could fail to process some inputs which is a different type of bug.

Why drag all this in here?  Ada, and for that matter GNAT come pretty close to this limit.  Applying theorem provers to parts of compilers or to parts of language definitions can improve the quality of compilers.  But anything that requires a language and a compiler for that language to be provably correct is just not possible.  (Actually you can accept a particular compiler as the definition of the language.  That eliminates one source of bugs by definition.  But along comes Gödel and some of his inconsistent numbers to rain on your party.  (Gödel's proofs rely on a mapping between partially recursive functions and integers.  Some numbers, for any mapping of PRFs to integers, will result in the (compiled code) stating that the function has the wrong output.  The simplest example is probably the halting function which cannot be correctly computed.  (If anyone ever tells you that there are some things which God did not want man to know, agree and point to the halting problem. If you don't believe in God, and think that man can know everything, you are still left with the halting problem. ;-) 

* It may be worth stating that limit here.  Regular expressions and finite state machines are languages beneath the bar.  For example, a compiler for arithmetic expressions can be proven true.  Add recursion, and you are over the line. 

Re: More reliable compilers (of some programming langauges) than GNAT

[Paul Rubin]

Robert Eachus <rieachus@comcast.net> writes:
> The problem is that for some recursive functions, it is not possible
> to prove that the input to the compiler (in Ada) and the output (in
> machine language) compute the same function for some partially
> recursive functions.

That makes no sense at all.  It's in general not possible to prove two
arbitrary programs produce the same output.  The input and output of the
Ada compiler are not arbitrary, but in fact they are closely related, so
nothing gets in the way of such a proof.  Look at CompCert
(compcert.inria.fr) for something like that being done with a C
compiler.  It would be great to use a similar approach for Ada.

Re: More reliable compilers (of some programming langauges) than GNAT

[Dmitry A. Kazakov]

On 23/11/2017 01:35, Randy Brukardt wrote:

> A "shared library" is not a "basic construct"; indeed, it is not an Ada
> construct at all so of course it has nothing to do with the quality of the
> *Ada* compiler.

Mot of the compiler, rather of the linker.

> Indeed, many Ada compilers don't bother to support "shared
> libraries"

GNAT supports shared libraries, not worse than Visual Studio does.

There is an issue with Windows DLL which must be addressed. When tasks 
are used explicitly or implicitly Ada RTL initialization will hang if 
done from PROCESS_ATTACH.

> as they are a rather useless construct that mainly serves to
> introduce bugs (if the shared library gets updated out of sync with
> the rest of the program).

There is no any alternative to shared libraries.

The problems lie mostly with loaders, linkers, differences in design 
(like having data in the library or not).

The problem of versioning, especially of elaborated interfaces like OO, 
exists no matter how you link your stuff.

Ada with SPARK could provide a huge qualitative step forward here, but 
that would also require total overhaul of existing linkers which are 
really remnants of 70's.

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

Re: More reliable compilers (of some programming langauges) than GNAT

[Dmitry A. Kazakov]

On 23/11/2017 04:40, Paul Rubin wrote:
> Robert Eachus <rieachus@comcast.net> writes:
>> The problem is that for some recursive functions, it is not possible
>> to prove that the input to the compiler (in Ada) and the output (in
>> machine language) compute the same function for some partially
>> recursive functions.
> 
> That makes no sense at all.  It's in general not possible to prove two
> arbitrary programs produce the same output.

Furthermore proof of compiler correctness has nothing to do with 
deciding which function is being computed. It is like deciding which 
source language it was from the machine code.

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

Re: More reliable compilers (of some programming langauges) than GNAT

[Robin]

"Victor Porton" <porton@narod.ru> wrote in message news:ov1fg0$15sq$1@gioia.aioe.org...
> Ada is good.
>
> But I have caught a few GNAT bugs while writing my software. It is too bad.
>
> Would you recommend me another language (not Ada) which has a quality free
> compiler?
>
> I need linking with C (like Ada Convention=>C), threads, containers library,
> and if possible reliability.
>
> Maybe should I switch to C++? Is C++ compiler more reliable than GNAT?
>
> I also heard of D and Swift. Huh?
>
> Java?
>
> Or (oh, oh, oh) plain C?

For a quality compiler, consider IBM's PL/I compiler.
However, it is not free. 



---
This email has been checked for viruses by Avast antivirus software.
https://www.avast.com/antivirus

Re: More reliable compilers (of some programming langauges) than GNAT

[Pascal Obry]

Le jeudi 23 novembre 2017 à 09:22 +0100, Dmitry A. Kazakov a écrit :
> There is an issue with Windows DLL which must be addressed. When
> tasks are used explicitly or implicitly Ada RTL initialization will
> hang if done from PROCESS_ATTACH.

That's a windows limitation. Nothing GNAT can do about.

-- 
  Pascal Obry /  Magny Les Hameaux (78)

  The best way to travel is by means of imagination

  http://www.obry.net

  gpg --keyserver keys.gnupg.net --recv-key F949BD3B

Re: More reliable compilers (of some programming langauges) than GNAT

[Dmitry A. Kazakov]

On 2017-11-23 17:14, Pascal Obry wrote:
> Le jeudi 23 novembre 2017 à 09:22 +0100, Dmitry A. Kazakov a écrit :
>> There is an issue with Windows DLL which must be addressed. When
>> tasks are used explicitly or implicitly Ada RTL initialization will
>> hang if done from PROCESS_ATTACH.
> 
> That's a windows limitation. Nothing GNAT can do about.

It can do task initialization of tasks outside PROCESS_ATTACH where 
threads are suspended. Presently the solution is to disable automatic 
initialization and call it manually at first use of the library 
interface. Clearly compiler can do that much better than programmer.

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

Re: More reliable compilers (of some programming langauges) than GNAT

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:ov60fj$mt8$1@gioia.aioe.org...
> On 23/11/2017 01:35, Randy Brukardt wrote:
...
>> as they are a rather useless construct that mainly serves to
>> introduce bugs (if the shared library gets updated out of sync with
>> the rest of the program).
>
> There is no any alternative to shared libraries.

Of course there is: write your code to use nothing but the target OS 
facilities and Ada. (Yes, I know that Windows uses shared libraries to 
implement the OS interface, but that's not visible to a statically linked 
program.) That was always the requirement at RRS, and any time that we've 
deviated from it we've generally come to regret it.

Statically linked programs are not going to fail because of some upgrade 
outside of botched OS upgrades (which are much less likely than other kinds, 
because most OS vendors are well aware of the havoc that they can cause).

The supposed reasons for using shared libraries rarely hold any water (there 
aren't going to be dozens of nearly identical Ada programs running on a 
single machine at a single time).

                                         Randy.

Re: More reliable compilers (of some programming langauges) than GNAT

[Dmitry A. Kazakov]

On 28/11/2017 02:09, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:ov60fj$mt8$1@gioia.aioe.org...
>> On 23/11/2017 01:35, Randy Brukardt wrote:
> ...
>>> as they are a rather useless construct that mainly serves to
>>> introduce bugs (if the shared library gets updated out of sync with
>>> the rest of the program).
>>
>> There is no any alternative to shared libraries.
> 
> Of course there is: write your code to use nothing but the target OS
> facilities and Ada. (Yes, I know that Windows uses shared libraries to
> implement the OS interface, but that's not visible to a statically linked
> program.) That was always the requirement at RRS, and any time that we've
> deviated from it we've generally come to regret it.

It does not work for any services, which stretch far beyond core OS. 
Basically if we were in 60's and everything would be standard I/O, you 
could ditch shared libraries, but now practically nothing is 
read/write/ioctl, but a call to some entry point in some shared library.

> Statically linked programs are not going to fail because of some upgrade
> outside of botched OS upgrades (which are much less likely than other kinds,
> because most OS vendors are well aware of the havoc that they can cause).

If somebody changes the parameters of ioctl or position where you read 
from or contents of the read data, your application will fail just the 
same. It is no matter how an interface to some external entity looks 
like. If the interface changes or if the external entity changes, you 
have a problem. Shared libraries provide much better interfaces than 
I/O. So they won, which is a good thing.

> The supposed reasons for using shared libraries rarely hold any water (there
> aren't going to be dozens of nearly identical Ada programs running on a
> single machine at a single time).

This applies only to pure computational components which are in minority 
and usually quite stable, because there is little reason why you would 
change interface of some solver. The majority of shared libraries is a 
combination of computations with some "monitor" part dealing with the 
outer world. You cannot have it static, it is impossible because of the 
second part. You could try to separate computation from the monitor, but 
that does not really work. E.g. GTK started as a separation of 
computational GUI from X11 I/O. Then it became an I/O itself and you 
have the same old problem again. Unless you pack everything into the OS 
and hold it there, you have no chance. The last who did that was DEC, 
long gone and dead. (DEC systems had perfect shared libraries too.)

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