3 ms·

> I suspect, though, that memory safety is one of the most important kinds of safety. I don't agree, at least in the context of safety that Ada is typically me

by orlp 3y ago

> I suspect, though, that memory safety is one of the most important kinds of safety. I don't agree, at least in the context of safety that Ada is typically mentioned in. Safety in this context is generally about human lives. Memory safety is by far the most important kind of safety against exploits. Because memory safety bugs lead to arbitrary code execution and a total security breakdown. However, where Ada is used most often - safety-critical and realtime systems in airplanes or medical equipment and such - most of the code is written for embedded systems. The attack surface is generally miniscule if any. The vast majority of issues that these contexts face I reckon are unit conversion errors, off-by-one errors, type overflows and logic errors.

cmrdporcupine 3y ago
Yes, this is exactly what I was getting at. The Rust static type system is actually not that rich for enforcing compile time constraints on values and states. It appears rich compared to C or Java or Go or something, but it's not that expressive even compared to languages in similar spaces like Scala or F# or even C++'s (rather terrifying) template system. This has advantages and disadvantages. But for the kind of thing we're talking about, there's some disadvantages. There are things a richer type constraints system could offer beyond even the 'range' constraints other people in this thread are referring to. e.g. I work on a (embedded-space) application that has a bunch of state machines in it. We naturally use Rust enums to describe these states. How nice it would be if Rust's enum system was rich enough to be able to describe and enforce the valid state transitions rather than just the set of possible states. There are various ways to try and approximate this (I've seen a few articles), but on the whole they're rather awkward and full of holes. Also the verbosity of Ada's syntax looks painful to write but actually pretty nice to read. This has got to have lots of value for paranoid organizations. I've seen plenty of terse and impenetrable Rust code, especially stuff that makes heavy use of rich static type action or funky things like GATs, etc.
- estebank 3y ago
  > We naturally use Rust enums to describe these states. How nice it would be if Rust's enum system was rich enough to be able to describe and enforce the valid state transitions rather than just the set of possible states. There are various ways to try and approximate this (I've seen a few articles), but on the whole they're rather awkward and full of holes. I'm assuming you're referring to type state machines, where you have one struct per state and the only way to translate from one state to the next is through method calls. Defining these is quite verbose (unless you rely on macros) but how is it full of holes?
  - cmrdporcupine 3y ago
    In that case: Potential holes because the permitted state transitions are scattered through function signatures and not described in a centralized place. You're right macros could make this more pleasant. I still think it's quite unergonomic. But yes, I probably should have said "awkward and/or full of holes" instead of and

by orlp 3y ago

cmrdporcupine 3y ago

Yes, this is exactly what I was getting at. The Rust static type system is actually not that rich for enforcing compile time constraints on values and states. It appears rich compared to C or Java or Go or something, but it's not that expressive even compared to languages in similar spaces like Scala or F# or even C++'s (rather terrifying) template system. This has advantages and disadvantages. But for the kind of thing we're talking about, there's some disadvantages. There are things a richer type constraints system could offer beyond even the 'range' constraints other people in this thread are referring to. e.g. I work on a (embedded-space) application that has a bunch of state machines in it. We naturally use Rust enums to describe these states. How nice it would be if Rust's enum system was rich enough to be able to describe and enforce the valid state transitions rather than just the set of possible states. There are various ways to try and approximate this (I've seen a few articles), but on the whole they're rather awkward and full of holes. Also the verbosity of Ada's syntax looks painful to write but actually pretty nice to read. This has got to have lots of value for paranoid organizations. I've seen plenty of terse and impenetrable Rust code, especially stuff that makes heavy use of rich static type action or funky things like GATs, etc.

estebank 3y ago
> We naturally use Rust enums to describe these states. How nice it would be if Rust's enum system was rich enough to be able to describe and enforce the valid state transitions rather than just the set of possible states. There are various ways to try and approximate this (I've seen a few articles), but on the whole they're rather awkward and full of holes. I'm assuming you're referring to type state machines, where you have one struct per state and the only way to translate from one state to the next is through method calls. Defining these is quite verbose (unless you rely on macros) but how is it full of holes?
- cmrdporcupine 3y ago
  In that case: Potential holes because the permitted state transitions are scattered through function signatures and not described in a centralized place. You're right macros could make this more pleasant. I still think it's quite unergonomic. But yes, I probably should have said "awkward and/or full of holes" instead of and