Interesting. The main reason I lost interest in Rust is because I found the type system to be too poor (there should be a better alternative to "rich" in this context, but I can't think of it right now).
Off the cuff, I'd say Ada addresses all of those problems. In case you're interested, I'll leave a few terms that might be useful in delving further.
- Nullable types + sum types. Pointers can be declared "not null" which basically works as it says. Sum types exist as discriminated and variant records. Variants can be immutable or mutable, and obviously work to do the typical Option, Result, etc stuff.
- Locked data. Protected types do this. I imagine details might differ, but I know nothing about how Rust does this and haven't messed with them much or at all in Ada.
- Task types. I'm tempted to say more, but the little details matter so much for this kind of thing so I probably shouldn't. But Ada has tasking and concurrency mechanisms built-in to the language.
- Typestate. Compiler errors for this sort of thing are not immediately obvious to me. I can think of several options to try using even just the features I already mentioned, but I'm not sure what would or would not be detectable at compile-time. Catching incorrect usage and preventing it from causing trouble is more trivial, but just not the same.
The simplest and (in my opinion) most important feature in Ada is the ability to trivially create new types. So many languages require manually wrapping types. Better ones start to provide more magic to help automate it. But fundamentally none of them make user-defined types as a core component of the language. In Ada to create a new type it's just one simple line, and you automatically get full functionality of the base type while retaining incompatibility. The rest of the language and even the standard library is all designed around the idea of allowing the programmer to freely use these types.
You end up capturing so much more of the model that the program is using, and the compiler is able to check and ensure that the code is actually sensible according to that model. I find even the process of writing the types down helps expose flaws in the design I had in my head. Then once I start using it, it does a great job of catching when I start deviating from how I said everything should work.
Pretty much every other language I've ever looked at makes doing that sort of thing extremely painful. There is too much friction involved in detailing all of that, so nobody does. Then libraries are designed without it, which just increases the friction. Ada meanwhile makes it so easy to do that you feel bad not doing it, and you don't even gain much more than saving a handful of keypresses if you avoid it anyway.
Off the cuff, I'd say Ada addresses all of those problems. In case you're interested, I'll leave a few terms that might be useful in delving further.
- Nullable types + sum types. Pointers can be declared "not null" which basically works as it says. Sum types exist as discriminated and variant records. Variants can be immutable or mutable, and obviously work to do the typical Option, Result, etc stuff.
- Locked data. Protected types do this. I imagine details might differ, but I know nothing about how Rust does this and haven't messed with them much or at all in Ada.
- Task types. I'm tempted to say more, but the little details matter so much for this kind of thing so I probably shouldn't. But Ada has tasking and concurrency mechanisms built-in to the language.
- Typestate. Compiler errors for this sort of thing are not immediately obvious to me. I can think of several options to try using even just the features I already mentioned, but I'm not sure what would or would not be detectable at compile-time. Catching incorrect usage and preventing it from causing trouble is more trivial, but just not the same.
The simplest and (in my opinion) most important feature in Ada is the ability to trivially create new types. So many languages require manually wrapping types. Better ones start to provide more magic to help automate it. But fundamentally none of them make user-defined types as a core component of the language. In Ada to create a new type it's just one simple line, and you automatically get full functionality of the base type while retaining incompatibility. The rest of the language and even the standard library is all designed around the idea of allowing the programmer to freely use these types.
You end up capturing so much more of the model that the program is using, and the compiler is able to check and ensure that the code is actually sensible according to that model. I find even the process of writing the types down helps expose flaws in the design I had in my head. Then once I start using it, it does a great job of catching when I start deviating from how I said everything should work.
Pretty much every other language I've ever looked at makes doing that sort of thing extremely painful. There is too much friction involved in detailing all of that, so nobody does. Then libraries are designed without it, which just increases the friction. Ada meanwhile makes it so easy to do that you feel bad not doing it, and you don't even gain much more than saving a handful of keypresses if you avoid it anyway.