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

141–150 of 173 posts

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

#141

Post by graealex »

graealex wrote: post #138
bluGill wrote: post #90

Earlier quoted context omitted.

Though if you do that km times km isn't km it is a volume - so your custom type would be wrong to have all operations. what unit km times km should be isn't clear.

These libraries already exist. God how people underestimate C++ all the time. Of course you can use a unit type that handles conversions AND mathematical operations. Feet to meter cubed and you get m³, and the library will throw a compile error if you try to assign it to anything it doesn't work with (liters would be fine, for example)

As a more general rant - people who have maybe used 5% of the feature set of C++ come along and explain why language X is superior because it has feature Y and Z.

News flash, C++ has every conceivable feature, it's the reason why it is so unwieldy. But you can even plug in a fucking GC if you so desire. Let alone stuff like basic meta programming.

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

#142

Post by OCTAGRAM »

usamoi wrote: post #8

I've never heard of SPARK. What advantages does it have compared to Lean?

They have different definitions of failure. In Lean a failure is to calculate wrong thing. In SPARK a failure is to not calculate at all because of memory issue or something like this. As far as I've seen SPARK, it encourages ephemeral data structures and effectful computations. Lean is less familiar to me, but I've got the impression that it is about correct computation in infinite memory and stack, and value-centered computations are encouraged. SPARK did not have pointers for long period. Then SPARK has got pointers, but only unique ones. Lean has shared pointers to immutable data structures. And infinitely recursive data structures.

Yet another provable code I have found in Eiffel. There is "proven" doubly linked list in Eiffel. Something not possible in SPARK, going against unique pointers. Something not possible in Lean, going against immutability.

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

#143

Post by 1718627440 »

pjmlp wrote: post #127
sgsjchs wrote: post #126

Earlier quoted context omitted.

But in C that's just syntax sugar for pointer math.

Except it is more obvious what is the intention, it is about clarity to the reader.

My point was indeed, that if you don't use pointer arithmetic in C, that means that you don't use arrays. I mean when you declare arrays of a fixed size, you can also declare an equivalent number of primitive variables instead, but I would find that inconvenient. Hence the question.

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

#145

Post by smj-edison »

1718627440 wrote: post #143
pjmlp wrote: post #127

Earlier quoted context omitted.

Except it is more obvious what is the intention, it is about clarity to the reader.

My point was indeed, that if you don't use pointer arithmetic in C, that means that you don't use arrays. I mean when you declare arrays of a fixed size, you can also declare an equivalent number of primitive variables instead, but I would find that inconvenient. Hence the question.

If I remember correctly, he meant that only array accesses are used, because their length can be checked (as all arrays have a static length due to no dynamic memory).

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

#146

Post by pezezin »

crims0n wrote: post #11

Alternatively, just get better at C/C++… It isn’t going anywhere, and it feels like more developers are coming around to the idea that maybe security guarantees are not worth throwing the baby out with the bath water.

Can we please stop with the "git gud" excuse? When even expert teams with decades of experience keep making mistakes, we need to recognize that C/C++ are fundamentally flawed and should be replaced with something better.

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

#147

Post by Jtsummers »

gosub100 wrote: post #107
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 needs to be "maintained" in a flying aircraft? If it's in need of an update, why was it certified to fly that way in the first place? Also in safety critical apps, being "difficult" can be a feature, not a big. Should we have easier turbofans so we can pop them open and swap out blades and rings for tiny little improvements? No. Every flight critical component should be fully understood as a prerequisite for use…

> why was it certified to fly that way in the first place?

Are you under the impression that software for aircraft is exceptionally good? A lot of the software for aircraft (for LRUs, avionics, whatever) are made by the same kind of developers as most other software.

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

#148

Post by uecker »

sgsjchs wrote: post #126
pjmlp wrote: post #102

Earlier quoted context omitted.

Like in most languages, with indexes.

But in C that's just syntax sugar for pointer math.

It still makes it possible to have bounds checking. (And it is also not true anymore for C2Y.)

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

#149

Post by uecker »

smj-edison wrote: post #145
1718627440 wrote: post #143

Earlier quoted context omitted.

My point was indeed, that if you don't use pointer arithmetic in C, that means that you don't use arrays. I mean when you declare arrays of a fixed size, you can also declare an equivalent number of primitive variables instead, but I would find that inconvenient. Hence the question.

If I remember correctly, he meant that only array accesses are used, because their length can be checked (as all arrays have a static length due to no dynamic memory).

Indeed, this is what many people do. But even if you use dynamic memory, if you replace pointer arithmetic by array indexing, you get bounds checking. And in C this also works for arrays of run-time length.

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

#150

Post by uecker »

Agingcoder wrote: post #58
jandrewrogers wrote: post #32

Earlier quoted context omitted.

Most of what gives high-reliability or high-assurance code that label is the process rather than the language. In colloquial terms it rigorously disallows sloppy code, which devs will happily write in any language given the chance. As much as C is probably the least safe systems language, and probably my last choice these days if I had to choose one, more high-assurance code has probably been written in C than any ot…

I don’t understand how you can get the same kind of reliability with C than with Spark - process or not, a formal proof is a formal proof. That’s much harder to get with C.

Why is it harder?
Post reply on HN