Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Ada and SPARK enter the automotive ISO-26262 market with Nvidia

adacore.com

Post reply on HN
Print view View original

31–40 of 113 posts

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#31

Post by pjmlp »

CivBase wrote: post #7
nabla9 wrote: post #6

Earlier quoted context omitted.

It was not for technical reasons. They needed more programmers and C++ had larger user base. Ada is technically better choice.

It has more to do with tooling than programmers. C++ is used everywhere so there are many commercial tools to support it. Not so much for Ada. Ada's developmemt tools are fewer, less featued, and more costly due to low demand.

There are 7 compiler vendors still in business, if anything Ada's domain is one of the fews where paying for tools one needs to do their job is still a thing, like in most professions.

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#32

Post by nabla9 »

CivBase wrote: post #14
johnisgood wrote: post #10

Earlier quoted context omitted.

> Ada's developmemt tools are fewer, less featued Such as?

Want a compiler? I hope you like GNAT. Want an IDE? I hope you like GNAT Pro Studio. Want a static analysis tool? I hope you like CodePeer. Want to do unit testing? I hope you like Rapita.

Ada compilers: PTC ApexAda, GreenHills Ada, Static analysis tools for Ada: CodePeer, ConQAT,Fluctuat,,LDRA Testbed,MALPAS,Polyspace,SofCheck Inspector,Squore,Understand. Similar list for all other things.

When C++ was chosen for F-35 there were more verification tools to Ada than C++.

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#33

Post by ryao »

dardeaup wrote: post #13
johnisgood wrote: post #10

Earlier quoted context omitted.

> Ada's developmemt tools are fewer, less featued Such as?

Regarding the number of options, C++ has quite a few IDEs: Visual Studio, Xcode, VSCode, CLion, and probably more (Oracle probably still sells the one they had for Solaris). For command-line compilers, C++ has: Visual Studio, Xcode, g++, clang++, IBM C++ compilers for their OSs, Oracle compilers for Solaris, etc. For Ada, is there anything other than AdaCore? Is that the same as GNATStudio? Edit* - fixed Ada capitali…

Netbeans is the Solaris IDE. It is free.

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#34

Post by whytevuhuni »

pjmlp wrote: post #29
atlgator wrote: post #16

Wow. I developed in Ada in aerospace 17 years ago. I thought the industry would move toward Rust.

5 years ago NVidia did not consider Rust mature enough for their use cases. This is the original announcement from 2020, "SPARK/Ada Journey to Adoption" https://youtu.be/DZSSyWlsb28?si=vh4gO-LT2N3Skaql Also we are now on Ada 202x already, quite different from Ada83, that some Rust folks keep comparing their favourite language with. You get all the niceties of a language more in line with Object Pascal productivity, f…

I don't know Ada / SPARK, and I've been trying to figure this out. Based on the hallucinations I got from ChatGPT, it seems Ada itself is nowhere near as powerful as Rust in safety, while Ada with SPARK disallows some things I was considering to be quite basic, such as shared aliasing of data.

For example, it seems it's not possible to get a sub-string slice reference to an original unbounded string. In rust, a &str -> &str signature is trivial.

So it seems Ada still relies on discipline, while SPARK does not have the zero-cost abstractions that C++ and Rust have.

If that's true (is it?), then I'd definitely choose C++/Rust over Ada any time, since performance is very important to me.

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#35

Post by pjmlp »

whytevuhuni wrote: post #34
pjmlp wrote: post #29

Earlier quoted context omitted.

5 years ago NVidia did not consider Rust mature enough for their use cases. This is the original announcement from 2020, "SPARK/Ada Journey to Adoption" https://youtu.be/DZSSyWlsb28?si=vh4gO-LT2N3Skaql Also we are now on Ada 202x already, quite different from Ada83, that some Rust folks keep comparing their favourite language with. You get all the niceties of a language more in line with Object Pascal productivity, f…

I don't know Ada / SPARK, and I've been trying to figure this out. Based on the hallucinations I got from ChatGPT, it seems Ada itself is nowhere near as powerful as Rust in safety, while Ada with SPARK disallows some things I was considering to be quite basic, such as shared aliasing of data. For example, it seems it's not possible to get a sub-string slice reference to an original unbounded string. In rust, a &str…

Less ChatGPT and more language reference manuals, ChatGPT isn't an ancient oracle knows it all, even though Microsoft's marketing sells it as such.

Ada has as much zero cost abstractions as C++ and Rust have, and one of the reasons of Ravenscar is even what to turn off for bare metal deployments, and real time OS deployments.

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#36

Post by anthk »

whytevuhuni wrote: post #34
pjmlp wrote: post #29

Earlier quoted context omitted.

5 years ago NVidia did not consider Rust mature enough for their use cases. This is the original announcement from 2020, "SPARK/Ada Journey to Adoption" https://youtu.be/DZSSyWlsb28?si=vh4gO-LT2N3Skaql Also we are now on Ada 202x already, quite different from Ada83, that some Rust folks keep comparing their favourite language with. You get all the niceties of a language more in line with Object Pascal productivity, f…

I don't know Ada / SPARK, and I've been trying to figure this out. Based on the hallucinations I got from ChatGPT, it seems Ada itself is nowhere near as powerful as Rust in safety, while Ada with SPARK disallows some things I was considering to be quite basic, such as shared aliasing of data. For example, it seems it's not possible to get a sub-string slice reference to an original unbounded string. In rust, a &str…

FFS, ChatGPT doesn't even has a clue on what is talking about.

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#37

Post by anthk »

pjmlp wrote: post #35
whytevuhuni wrote: post #34

Earlier quoted context omitted.

I don't know Ada / SPARK, and I've been trying to figure this out. Based on the hallucinations I got from ChatGPT, it seems Ada itself is nowhere near as powerful as Rust in safety, while Ada with SPARK disallows some things I was considering to be quite basic, such as shared aliasing of data. For example, it seems it's not possible to get a sub-string slice reference to an original unbounded string. In rust, a &str…

Less ChatGPT and more language reference manuals, ChatGPT isn't an ancient oracle knows it all, even though Microsoft's marketing sells it as such. Ada has as much zero cost abstractions as C++ and Rust have, and one of the reasons of Ravenscar is even what to turn off for bare metal deployments, and real time OS deployments.

Seriously, if these people use ChatGPT to seek new knowledge, we are doomed. They are utterly clueless.

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#38

Post by Agingcoder »

whytevuhuni wrote: post #34
pjmlp wrote: post #29

Earlier quoted context omitted.

5 years ago NVidia did not consider Rust mature enough for their use cases. This is the original announcement from 2020, "SPARK/Ada Journey to Adoption" https://youtu.be/DZSSyWlsb28?si=vh4gO-LT2N3Skaql Also we are now on Ada 202x already, quite different from Ada83, that some Rust folks keep comparing their favourite language with. You get all the niceties of a language more in line with Object Pascal productivity, f…

I don't know Ada / SPARK, and I've been trying to figure this out. Based on the hallucinations I got from ChatGPT, it seems Ada itself is nowhere near as powerful as Rust in safety, while Ada with SPARK disallows some things I was considering to be quite basic, such as shared aliasing of data. For example, it seems it's not possible to get a sub-string slice reference to an original unbounded string. In rust, a &str…

Both Ada and spark have zero costs abstractions, they’re designed to run on embedded platforms.

Spark is a different use case from rust - it’s a full prover, and the goal is formal verification, typically in contexts where human life is at stake ( say, you’re writing software for an artificial heart , to take an extreme example ). This comes at the cost of being less flexible, but they’ve been slowly evolving spark so that it can handle increasingly complex cases .

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#39

Post by sam_bristow »

CivBase wrote: post #14
johnisgood wrote: post #10

Earlier quoted context omitted.

> Ada's developmemt tools are fewer, less featued Such as?

Want a compiler? I hope you like GNAT. Want an IDE? I hope you like GNAT Pro Studio. Want a static analysis tool? I hope you like CodePeer. Want to do unit testing? I hope you like Rapita.

For C++ on similar systems its becoming more and more "I hope you like LLVM with the serial numbers filed off". Lots of the tool vendors are sunsetting their bespoke compilers. Most of the vendor IDEs have always been Eclipse with a bunch of bundled plugins.

Re: Ada and SPARK enter the automotive ISO-26262 market with Nvidia

#40

Post by DoingIsLearning »

pjmlp wrote: post #29
atlgator wrote: post #16

Wow. I developed in Ada in aerospace 17 years ago. I thought the industry would move toward Rust.

5 years ago NVidia did not consider Rust mature enough for their use cases. This is the original announcement from 2020, "SPARK/Ada Journey to Adoption" https://youtu.be/DZSSyWlsb28?si=vh4gO-LT2N3Skaql Also we are now on Ada 202x already, quite different from Ada83, that some Rust folks keep comparing their favourite language with. You get all the niceties of a language more in line with Object Pascal productivity, f…

> industry baremetal profiles like Ravenscar

I understand the value proposition of Formal Verification with Spark.

But for me the killer features with Ada, thinking specifically of embedded systems is:

- The expressiveness you gain with Ada's Type System

- The Ravenscar profile (very impressive work from a small group of folks in the IRTAW group)

Post reply on HN