Live data from Hacker News

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

adacore.com

71–80 of 113 posts

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

#71
post #67

Earlier quoted context omitted.

I have worked on safety crucial systems and applications that interact with safety critical systems in a non safety critical language. Each time it never had anything to do with the language and everything to do with systems engineering and project management. The projects that were successful had excellent systems engineering and project management. Language choice was never a factor.

This is my experience as well. People need to ask themselves what benefits Rust would bring to an high assurance system (e.g. DO-178C Level A). You're not gonna want to malloc mid-flight even if you have a borrow checker. The entire point of e.g. DO-178C is to show that the software only does exactly what it is supposed to do under all assumptions and have any derived behavior fed back to the safety process for evalu…

I personally know of teams using modern tooling and expansive cloud based CI/CD with safety critical systems and we are talking hundreds of developers. This is in C++ with MISRA standards and DO-178 too.

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

#72
post #51
post #45

Earlier quoted context omitted.

To be fair to ChatGPT, trying to find good documentation for Ada +/- Spark hasn't been quite as smooth sailing as trying to find something for C++. > Ada has as much zero cost abstractions as C++ and Rust have. Couldn't find anything about it (see above), but does Ada come with any monomorphization tricks?

What does that to do with zero cost abstractions as described originally by Bjarne Stroustroup? The way generics are implemented in Ada compilers is implementation specific.

How exactly are you going to implement generics in a way that's:

> What you don’t use, you don’t pay for. And further: What you do use, you couldn’t hand code any better.

without monomorphizing the generics?

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

#73
post #8

Earlier quoted context omitted.

Everything I've heard about it was that it was pressure from contractors because they didn't like training or finding Ada talent. I get that there's more tools for C++ but first class formal verification support and a language that's generally designed to save you from yourself seems like something you would stand your ground on. Ada is supremely good at killing people and/or keeping them un-killed, there's a reason…

>Everything I've heard about it was that it was pressure from contractors because they didn't like training or finding Ada talent. Do you think the auto industry will have a easier time finding Ada talent at their pay rates? Or that talent will want to specialize into Ada just to pigeonhole themselves into the Automotive jobs market?

I'm near Detroit which has a huge amount of auto industry, and engineering pay is good across pretty much all disciplines. It'll pay for a happy life and then some as long as relentless title climbing and job hopping isn't your definition of happiness.

Ada is not some exotic thing that requites SF comp. If it's such a major adjustment coming from C/C++ that it's actually causing you trouble, you have other problems.

It's comical bringing up the automotive industry considering that its responsible for AUTOSAR, which is simultaneously widely hated by engineers and completely useless outside the industry.

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

#74

Earlier quoted context omitted.

THIS. I knew someone a while back who worked on Patriot missile software. It was Ada. And Patriot still a formidable weapon.

You mean the Patriot that ended up getting 28 people killed due to a SW bug?[1] That Patriot? Let me repeat myself again, Ada won't save you from human bugs. If you hire bad programmers or have bad dev and test practices, there's no magic programming language that will save you from your calculation and logic mistakes. You can code in raw machine code like you're 1960's NASA, and still have less bugs than a clueless…

The Patriot failures were the result of floating point error. Ada provides facilities specifically to deal with this, while you're left rolling your own in C/C++. Of course Ada won't save you from human bugs, but it's silly to say that you're no better off with a language giving you everything it can to avoid them than one that is a notorious fuckup dispenser.

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

#75
post #41

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…

I don't think a single point there is true. Ada has had shared aliases since 1995. Its had zero cost abstractions since before then. Slicing memory from a string is in the intro manual, for example. my_var(2 .. 6) Ada doesn't rely on you to be disciplined. [0] Memory safety comes with SPARK. Its a theorum prover. [0] https://blog.adacore.com/memory-safety-in-ada-and-spark-thro...

But doesn't this copy the entirety of that slice? That's not what I meant, I was referring to a shared reference, akin to &str in Rust or std::string_view in C++.

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

#76
post #41

Earlier quoted context omitted.

I don't think a single point there is true. Ada has had shared aliases since 1995. Its had zero cost abstractions since before then. Slicing memory from a string is in the intro manual, for example. my_var(2 .. 6) Ada doesn't rely on you to be disciplined. [0] Memory safety comes with SPARK. Its a theorum prover. [0] https://blog.adacore.com/memory-safety-in-ada-and-spark-thro...

But doesn't this copy the entirety of that slice? That's not what I meant, I was referring to a shared reference, akin to &str in Rust or std::string_view in C++.

Doing it normally should create a copy of the value, as far as I can tell. Unless you use it to create a renamed variable or by-reference parameter, the same way you can create references in C++.

I think the closest thing to a &str in Ada would be an "access String" or "access constant String", which you would get either from an allocated "String" or from a declared "aliased String". You'd create a subslice with "string(x..y)'Access". Though I'm not sure whether that actually works without explicitly declaring an array of "aliased Character", the Manual is dense (as with C++, it's nearly meaningless unless you already know what it's supposed to mean) and the tutorials generally avoid talking about access objects.

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

#77
post #72
post #51

Earlier quoted context omitted.

What does that to do with zero cost abstractions as described originally by Bjarne Stroustroup? The way generics are implemented in Ada compilers is implementation specific.

How exactly are you going to implement generics in a way that's: > What you don’t use, you don’t pay for. And further: What you do use, you couldn’t hand code any better. without monomorphizing the generics?

By letting the compilers decide the best way to implement them.

Also I find funny this point of view on Ada, given the poor examples WG21 has added into the C++ standard library, that will never be fixed due to never-ending ABI drama.

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

#78

Earlier quoted context omitted.

But doesn't this copy the entirety of that slice? That's not what I meant, I was referring to a shared reference, akin to &str in Rust or std::string_view in C++.

Doing it normally should create a copy of the value, as far as I can tell. Unless you use it to create a renamed variable or by-reference parameter, the same way you can create references in C++. I think the closest thing to a &str in Ada would be an "access String" or "access constant String", which you would get either from an allocated "String" or from a declared "aliased String". You'd create a subslice with "str…

Thank you! I assume 'Access types are not memory-safe, right? Is there a SPARK equivalent which still does not copy (i.e. it only references) that is memory safe?

To be more specific, how would one implement something like a "Get_First_Word" or "Trim_Whitespace" without copying?

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

#79

Earlier quoted context omitted.

Doing it normally should create a copy of the value, as far as I can tell. Unless you use it to create a renamed variable or by-reference parameter, the same way you can create references in C++. I think the closest thing to a &str in Ada would be an "access String" or "access constant String", which you would get either from an allocated "String" or from a declared "aliased String". You'd create a subslice with "str…

Thank you! I assume 'Access types are not memory-safe, right? Is there a SPARK equivalent which still does not copy (i.e. it only references) that is memory safe? To be more specific, how would one implement something like a "Get_First_Word" or "Trim_Whitespace" without copying?

I think it's supposed to be safe in Ada by default? As far as I can tell, basic allocated objects cannot be deallocated without an "unchecked" operation, and access objects created from "aliased" declarations are subject to scoping rules [0]. (If you want to know the full details, go figure out however "accessibility levels" are supposed to work [1].) It should preclude functions from returning access objects without a "prefix'Unchecked_Access" operation. I'm not sure how SPARK's borrowing system is tied into all of this.

[0] https://www.adaic.org/resources/add_content/docs/craft/html/...

[1] http://www.ada-auth.org/standards/22rm/html/RM-3-10-2.html

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

#80
post #77
post #72

Earlier quoted context omitted.

How exactly are you going to implement generics in a way that's: > What you don’t use, you don’t pay for. And further: What you do use, you couldn’t hand code any better. without monomorphizing the generics?

By letting the compilers decide the best way to implement them. Also I find funny this point of view on Ada, given the poor examples WG21 has added into the C++ standard library, that will never be fixed due to never-ending ABI drama.

Look. I'm not against Ada. Not my favorite language but definitely huge step in the right direction.

With that said. How does:

> By letting the compilers decide the best way to implement them.

Get you to zero cost generics. What if implementor just says "let them eat memory" and boxes the generic.

Post reply on HN