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

91–100 of 173 posts

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

#91

Post by nosianu »

MichaelEstes wrote: post #82

I might be in the minority, but I hate type re-definitions, I want types to just tell me how much memory a variable is using and it’s bit interpretation. Every variable already has a name, use that to communicate the data’s representation and if it’s really important that representation mismatches are caught at compile time wrap it in a struct. I don’t want to guess how much memory the compiler decided a variable nee…

Understandable. Many many years ago I sat in front of a commercial code base for the very first time, a well-known large database company, and my first despair-level was reached quickly when I saw that everybody who ever submitted a patch seemed to have created their own version of very basic types such as 32 bit unsigned integers, making following the code and checking the types on the way very hard.

On the other hand, these kinds of types for different kinds of numbers are meant for higher-level checks. Not confusing some random number with a monetary amount, or, as in the example, miles with kilometers, sure helps. The latter might have prevented that Mars mission that failed due to such a unit error (Mars Climate Orbiter).

The problem, as so often, is that we only have one source code (level), but very different levels of abstraction. Similar when you try to add very low-level things like caching, that have to be concerned with implementation and hardware, and mix it with business logic (alternative: even more abstraction and code to try to separate the two, but then you will have more indirection and less knowledge of what is really going on when you need to debug something).

Sometimes you are interested in the low-level concepts, such as number of bytes, but other types you want some higher level ideas expressed in your types. Yet, we only have one type layer and have to put it all in there, or choose only one and then the other kind of view suffers.

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

#92

Post by debugnik »

saraaah wrote: post #81
AlotOfReading wrote: post #56

Earlier quoted context omitted.

C and C++ don't have such a subset. That seems pretty relevant, given they're the languages being compared and they're used for the majority of safety critical development. The standards I mentioned use tricks to get around this. MISRA, for example, has the infamous rule 1.3 that says "just don't do bad things". Actually following that or verifying compliance are problems left completely to the user. On the other han…

Memory safety doesn't really help that much with functional safety. Sure, a segfault could potentially make some device fail to do its safety critical operation, but that is treated in the same way a logic bug would be, so it's not really a concern in of itself. But then again, an unchecked .unwrap() would lead to the same failure mode, so a "safe" crash just just as bad as an "unsafe" one.

But memory-unsafe code doesn't just segfault, it can corrupt your invariants and continue running, or open a door for an attacker to RCE on the machine. Memory safety is necessary (but not sufficient) to uphold what should be the simplest invariant of any code base, that program execution matches the source code in the first place.

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

#93

Post by pjmlp »

bluGill wrote: post #90
NekkoDroid wrote: post #83

Earlier quoted context omitted.

In C++ you probably could even make a templated class that implements all possible operators for any type that supports it with concepts. Then you can just `using kilometer = unique_type ` without needing to create a custom type each time.

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.

Thankfully some folks already thought that out, one possible library,

https://mpusz.github.io/mp-units/latest/

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

#94

Post by pjmlp »

bitwize wrote: post #33
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?

You can actually do this in C as well. The Windows API has all sorts of handle types that were originally all one type: HANDLE; but by wrapping a HANDLE in various one-member structs were able to derive different handle types that couldn't be intermixed with each other in a type-safe way without some casting jiggery-pokery. It's just much, much easier and more ergonomic in Ada.

Fun fact, that many are not aware, mostly because this is Windows 3.x knowledge and one needed the right source to learn about this.

There was a header only library on the Windows SDK that would wrap those HANDLEs into more specific types, that would still be compatible, while providing a more high level API to use them from C.

Unfortunely there is not much left on the Internet about it, but this article provides some insight,

https://www.codeguru.com/windows/using-message-crackers-in-t...

Naturally it was saner just to use TP/C++ alongside OWL, C++ with MFC back then, or VB.

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

#95

Post by secondcoming »

NekkoDroid wrote: post #83
platinumrad wrote: post #48

Earlier quoted context omitted.

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.

In C++ you probably could even make a templated class that implements all possible operators for any type that supports it with concepts. Then you can just `using kilometer = unique_type ` without needing to create a custom type each time.

C++ really needs something like `using explicit kilometer = uint32_t;`

The 'explicit' would force you to use static_cast

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

#96

Post by rramadass »

One can learn to apply Formal Methods at many levels in any language using available tools at hand. For some ideas see;

1) On Formal Methods Thinking in Computer Science Education - https://dl.acm.org/doi/10.1145/3670419

2) (In-)Formal Methods: The Lost Art --- A Users’ Manual by Carroll Morgan - https://fme-teaching.github.io/2019/10/03/in-formal-methods-...

3) Forthcoming book by Carroll Morgan Formal Methods, Informally How to Write Programs That Work - https://www.cambridge.org/highereducation/books/formal-metho...

4) Understanding Formal Methods by Jean-Francois Monin - A firehose of information.

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

#97

Post by ajxs »

vouwfietsman wrote: post #45
ajxs wrote: post #41

Earlier quoted context omitted.

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

> 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?

You're right. Validating input is a part of this process. The compiler can trivially disprove that the array can be safely indexed by the full set of any valid integer that the user can input. Adding a runtime check to ensure we have a valid index isn't a very impressive use of formal proofs, I admit. It's just a simple example that clearly demonstrates how SPARK can prove 'memory-safety' properties.

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

#98

Post by GreenWatermelon »

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.

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.

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

#100

Post by pjmlp »

HelloNurse wrote: post #73
boxed wrote: post #66

Earlier quoted context omitted.

Aside from technical factors, there are social factors involved. For example, both Python and C++ has operator overloading. But in C++ that's horrible and you run screaming from it, while in Python land it's perfectly fine. What is the difference? Culture and taste.

It isn't the same operator overloading. In C++ operator overloading can easily mess with fundamental mechanisms, often intentionally; in Python it is usually no more dangerous than defining regular functions and usually employed purposefully for types that form nice algebraic structures.

I hardly see the difference, given the capabilities of operator overloading in Python,

    class MyNum(int):
        def __add__ (self, other):
            return super().__add__(other) * 10
        
        
    n = MyNum(12)
    a = 45
    print(n + a) # oops
Post reply on HN