Remix.run Logo
skepti2 2 days ago

> Ada and especially Spark makes it a whole lot easier to produce correct software.

Relative to what? There are formal verification tools for other languages. I have heard Ada/SPARK is good, but I do not know the veracity of that. And Ada companies promoting Ada have horses in the race.

And Ada didn't prevent the Ada code in Ariane 5 from being a disaster.

> The programming language is just a small piece of the puzzle. But an important one.

100% true, but the parent of the original post that he agreed with said:

> And the F35 and America's combat readiness would be in a better place today with Ada instead of C++.

What is the proof for that, especially considering events like Ariane 5?

And Ada arguably has technical and non-technical drawbacks relative to many other languages.

When I tried Ada some weeks ago for a tiny example, I found it cumbersome in some ways. Is the syntax worse and more verbose than even C++? Maybe that is just a learning thing, though. Even with a mandate, Ada did not catch on.

serf 2 days ago | parent | next [-]

>What is the proof for that, especially considering events like Ariane 5?

Ariane 5 is a nice anti-ada catchphrase, but ada is probably the most used language for war machines in the United States.

now the argument can be whether or not the US military is superior to X; but the fact that the largest military in the world is filled to the brim with warmachines running ada code is testament itself to the effectiveness of the language/dod/grant structure around the language.

would it be better off in c++? I don't know about that one way or the other , but it's silly pretend ada isn't successful.

skepti2 2 days ago | parent [-]

But Ada had for a number of years a mandate to require its usage [0]. That should have been an extreme competitive advantage. And even then, C++ is still used these days for some US military projects, like F-35. Though I don't know whether the F-35 is successful or not, if it is not, that could be an argument against C++.

Ada is almost non-existent outside its niche.

The main companies arguing for Ada appear to be the ones selling Ada services, meaning they have a horse in the race.

I barely have any experience at all with Ada. My main impression is that it, like C++, is very old.

[0]: https://www.militaryaerospace.com/communications/article/167...

> The Defense Department`s chief of computers, Emmett Paige Jr., is recommending a rescission of the DOD`s mandate to use the Ada programming language for real-time, mission-critical weapons and information systems.

galangalalgol 2 days ago | parent [-]

Poking around it looks like ada is actually the minority now. Everything current is either transitioning to c++ or started that way. The really old but still used stuff is often written in weird languages like jovial or in assembly.

p_l 2 days ago | parent [-]

Essentially the story of DoD mandates goes down to everyone getting waivers all the time and nuking the mandate.

yoda222 2 days ago | parent | prev | next [-]

> Ada didn't prevent the Ada code in Ariane 5 from being a disaster

That's a weak argument to say that Ada could not lead to a better place in term of software. It's like saying that it's not safer to cross at a crosswalk because you know someone who died while crossing on one.

(But I guess that's fair for you to say that, as the argument should probably be made by the people that say that Ada would be better, and because they made a claim without evidences, you can counterclaim without any evidence :-) )

There are no programming language that can prevent a software for working correctly outside of the domain for which the software is written, which was the case for Ariane 501. Any language that would have been used to write the same software for Ariane 4 may have led to the same exact error. Ariane 501 failure is a system engineering problem here, not a software problem (even if in the end, the almost last piece in the chain of event is a software problem)

zeroc8 2 days ago | parent | prev | next [-]

Well, readability, better typesafety, less undefined behaviour. In and out parameters, named parameters. Built in concurrency.

With C++ it's just too easy to make mistakes.

IshKebab 2 days ago | parent | prev [-]

> Relative to what?

Relative to C++.

> There are formal verification tools for other languages.

None that are actually used.

I have no horse in this race and I have never actually written any Ada, but it seems pretty clear to me that it would produce more correct code on average.

Looking at the Ariane 5 error it looks like the specifically disabled the compile-time error: https://www.sarahandrobin.com/ingo/swr/ariane5.html

That's nothing to do with Ada.

Also asking for evidence is a red herring. Where's the evidence that Rust code is more likely to be correct than Perl? There isn't any. It's too difficult to collect that evidence. Yet it's obviously true.

Plenty of things are pretty obviously true but collecting scientific evidence of them is completely infeasible. Are code comments helpful at all? No evidence. Are regexes error-prone and hard to read? No evidence. Are autoformatters helpful? No evidence.