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

Should I choose Ada, SPARK, or Rust over C/C++? (2024)

blog.adacore.com

Post reply on HN
Print view View original

41–50 of 173 posts

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#41

Post by ajxs »

waterTanuki wrote: post #38

> If you’re prepared to look at alternative programming languages to avoid the costs and risks of C/C++, SPARK offers an opportunity to go much further than Ada or Rust. SPARK, which is based on Ada, offers industrial-strength formal methods: an opportunity for you to prove mathematically that your software is safe and secure. This paradigm shift in software development methodology offers significant cost savings for…

> Regardless of the language, you cannot write some special program that guarantees an input will be valid if it comes from an external source or a human. It is simply impossible to prove this at compile time.

> ...but from my perspective it looks worse in Ada...

This isn't really true. SPARK obviously can't prove that the input will be valid, but it can formally prove that the validity of the user input is verified before it's used.

I wrote about this here: https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Aga...

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#42

Post by AlotOfReading »

oguz-ismail wrote: post #39
ecshafer wrote: post #22

Earlier quoted context omitted.

It is not saying that it is not possible to make C code that is safe enough to be on an airplane. Its that there are languages with additional features which make it easier to have a high confidence. If you can remove entire classes of bugs automatically, why not do so?

> Its that there are languages with additional features which make it easier to have a high confidence. If you can remove entire classes of bugs automatically, why not do so? Which languages remove which classes of bugs entirely? This vagueness is killing me

Safe Rust and Ada SPARK entirely remove classes of bugs like undefined behavior and memory safety issues. The latter will also statically eliminate things like overflow and type range errors.

These are subsets of their respective languages, but all safety critical development in C and C++ relies on even more constrained language subsets (e.g. MISRA or AV++) to achieve worse results.

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#44

Post by 112233 »

markasoftware wrote: post #13

Their example of why Ada has better strong typing than Rust is that you can have floats for miles and floats for kilometers and not get them mixed up. News flash, Rust has newtype structs, and you can also do basically the same thing in C++. I don't know much about Ada. Is its type system any better than Rust's?

I'm super interested how you can do this in C++. Say, I need aggregate struct with a few 16 and 32 bit fields, some are little endian and some big endian. I do not want C++ to let me mix up endianness. How do I do it?

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#45

Post by vouwfietsman »

ajxs wrote: post #41
waterTanuki wrote: post #38

> If you’re prepared to look at alternative programming languages to avoid the costs and risks of C/C++, SPARK offers an opportunity to go much further than Ada or Rust. SPARK, which is based on Ada, offers industrial-strength formal methods: an opportunity for you to prove mathematically that your software is safe and secure. This paradigm shift in software development methodology offers significant cost savings for…

> Regardless of the language, you cannot write some special program that guarantees an input will be valid if it comes from an external source or a human. It is simply impossible to prove this at compile time. > ...but from my perspective it looks worse in Ada... This isn't really true. SPARK obviously can't prove that the input will be valid, but it can formally prove that the validity of the user input is verified…

I am no expert here what I remember is mostly from CS courses, but isn't the entire point of a formal program proof that you can reason about the combinatorics of all data and validate hypothesis on those?

It's one thing to say: "objects of this type never have value X for field Y", or "this function only works on type U and V", but its a lot more impressive to say "in this program state X and Y are never achieved simultaneously" or "in this program state X is always followed by state Y".

This is super useful for safety systems, because you can express safety in these kinds of functions that are falsifiable by the proof system. E.g: "the ejection seat is only engaged after the cockpit window is ejected" or "if the water level exceeds X the pump is always active within 1 minute".

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#46

Post by oguz-ismail »

AlotOfReading wrote: post #42
oguz-ismail wrote: post #39

Earlier quoted context omitted.

> Its that there are languages with additional features which make it easier to have a high confidence. If you can remove entire classes of bugs automatically, why not do so? Which languages remove which classes of bugs entirely? This vagueness is killing me

Safe Rust and Ada SPARK entirely remove classes of bugs like undefined behavior and memory safety issues. The latter will also statically eliminate things like overflow and type range errors. These are subsets of their respective languages, but all safety critical development in C and C++ relies on even more constrained language subsets (e.g. MISRA or AV++) to achieve worse results.

> These are subsets of their respective languages, but

Pretty much every language has such a subset. Nothing new then, sigh...

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#47

Post by rendaw »

firesteelrain wrote: post #7

I know there is a belief that Rust/Ada etc is safer than C/C++ and in some cases that is true. I know of multiple, airworthy aircraft that are flying with C++ code. I also know of aircraft flying with Ada. The aircraft flying with Ada is hard to maintain. There is also a mountain of testing that goes into it that is not just unit testing. This mountain of integration, subsystem and system level testing is required re…

What makes Ada harder to maintain? Do you have a source for that so I could read more?

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#48

Post by platinumrad »

112233 wrote: post #44
markasoftware wrote: post #13

Their example of why Ada has better strong typing than Rust is that you can have floats for miles and floats for kilometers and not get them mixed up. News flash, Rust has newtype structs, and you can also do basically the same thing in C++. I don't know much about Ada. Is its type system any better than Rust's?

I'm super interested how you can do this in C++. Say, I need aggregate struct with a few 16 and 32 bit fields, some are little endian and some big endian. I do not want C++ to let me mix up endianness. How do I do it?

C: struct be32_t { uint32_t _ }; struct le32_t { uint32_t _ };

C++: That, but with a billion operator overloads and conversion operators so they feel just like native integers.

Re: Should I choose Ada, SPARK, or Rust over C/C++? (2024)

#50

Post by waterTanuki »

ajxs wrote: post #41
waterTanuki wrote: post #38

> If you’re prepared to look at alternative programming languages to avoid the costs and risks of C/C++, SPARK offers an opportunity to go much further than Ada or Rust. SPARK, which is based on Ada, offers industrial-strength formal methods: an opportunity for you to prove mathematically that your software is safe and secure. This paradigm shift in software development methodology offers significant cost savings for…

> Regardless of the language, you cannot write some special program that guarantees an input will be valid if it comes from an external source or a human. It is simply impossible to prove this at compile time. > ...but from my perspective it looks worse in Ada... This isn't really true. SPARK obviously can't prove that the input will be valid, but it can formally prove that the validity of the user input is verified…

This is the smoking gun for me:

    procedure Overflow_This_Buffer
       with SPARK_Mode => On
    is
       type Integer_Array is array (Positive range ) of Integer;
       Int_Array : Integer_Array (1 .. 10) := [others => 1];
       Index_To_Clear : Integer;
    begin
       Ada.Text_IO.Put ("What array index should be cleared? ");
       --  Read the new array size from stdin.
       Ada.Integer_Text_IO.Get (Index_To_Clear);

       Int_Array (Index_To_Clear) := 0;
    end Overflow_This_Buffer;
What I am asking is what exactly is formally proving from 1st principles? Because to me this looks no different than a simple assertion statement or runtime bounds check which can be performed in any language with if statements & exceptions.

How did you prove that no one could just put in an arbitrary integer into that function? Does it fail to compile? Then you're just making a custom type which enforces valid state which, again can be done in any language with a rich type system and if statements.

If I might be more blunt: formal proofs in the field of programming appear to be nothing more than mathematicians trying to strong-arm their way into the industry where they aren't necessarily needed. Formal proofs make sense when you're trying to come up with new formulas or studying the cosmos, but they make no sense when you're trying to predict how bits will behave on a computer, because for the most part that is a solved problem by languages themselves.

Post reply on HN