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

121–130 of 173 posts

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

#121

Post by morshu9001 »

zeroc8 wrote: post #77
morshu9001 wrote: post #55

Earlier quoted context omitted.

Go's biggest flaw for backends is the error handling. No exceptions and nothing checking that you use the err. Java's issue might be the lack of cooperative multitasking until recently (virtual threads). Best you could do was those promises frameworks that mangle your code, and Google in particular uses something a hundred times worse called Guice (which is also DI).

Java's biggest problem is the fact that mutability is so baked into the language. I'm working on a project now where I always need to dig deep to find out if something has been mutated or not. Yes, there are records and we are now getting into data oriented programming. But older codebases are really hard to read.

One of the classic problems with OOP

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

#122

Post by morshu9001 »

GreenWatermelon wrote: post #98
zeroc8 wrote: post #77

Earlier quoted context omitted.

Java's biggest problem is the fact that mutability is so baked into the language. I'm working on a project now where I always need to dig deep to find out if something has been mutated or not. Yes, there are records and we are now getting into data oriented programming. But older codebases are really hard to read.

Java also has (In my experience) a higher concentration of inept developers who seem to have never heard of guard conditiona and early returns, and prefer instead to wrap everything in if conditions, pushing the actual logic into deeper nesting levels. Pyramids of doom all over.

Yeah but there are way more inept devs using JS, and I still have an easy time understanding JS codebases. Java seems to encourage overabstraction and weird frameworks.

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

#124

Post by zeroc8 »

morshu9001 wrote: post #121
zeroc8 wrote: post #77

Earlier quoted context omitted.

Java's biggest problem is the fact that mutability is so baked into the language. I'm working on a project now where I always need to dig deep to find out if something has been mutated or not. Yes, there are records and we are now getting into data oriented programming. But older codebases are really hard to read.

One of the classic problems with OOP

One of the biggest mistake we've made as an industry. The good thing is that the worst days are over. The whole design pattern craze was pretty annoying, to say the least.

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

#125

Post by sgsjchs »

forthac wrote: post #25
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?

This was posted to about a day ago: https://github.com/johnperry-math/AoC2023/blob/master/More_D... But a noteworthy excerpt: ``` Ada programs tend to define types of the problem to be solved. The compiler then adapts the low-level type to match what is requested. Rust programs tend to rely on low-level types. That may not be clear, so two examples may help: Ada programmers prefer to specify integer types in terms of…

You very rarely would actually want scalar types which don't map directly to hardware supported ones anyway.

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

#129

Post by jordanb »

6r17 wrote: post #6
jordanb wrote: post #3

I found that learning Ada was a good way to learn how to write good C++ code, because both languages are at the same level of abstraction but Ada is clean and opinionated. The best a example is RAII. This is a pattern in C++ that you have to follow if you don't want to make a mess. In Ada it's a language feature called Controlled Types.

Do you feel the same is true for someone who does mainly rust nowadays ? I had the same feeling with rust & python ; If there are any patterns that help in other languages I'd definitely like to look them up

I don't know Rust so I can't comment on it.

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

#130

Post by vouwfietsman »

waterTanuki wrote: post #52
vouwfietsman wrote: post #45

Earlier quoted context omitted.

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 si…

But isn't the entire point of rust's verbose type system to declare valid states at compile time? I don't exactly see how this can't be proved in rust.

I am not a Rust expert either, but just a general remark: using a programming language like Rust as its intended to be used, i.e. functional/imperative programming of the problem domain, does not lend itself well to proving/disproving the kind of statements I showed above.

Yes, you could theoretically generate a Rust program that does not compile if some theorem does not hold, but this is often times (unless the theorem is about types) not a straightforward Rust program for the problem at hand.

I also think that, although Rust is blurring the lines a bit, equating formal verification and type-checking is not a valid stance. A type checker is a specific kind of formal verification that can operate on a program, but it will only ever verify a subset of all hypotheses: those about object types.

Post reply on HN