fghfghgfhfg
Joined 11 years ago
Joined 11 years ago
You have to jump through the same sort of hoops in Rust as you do C++ to get the sort of basic type safety found in Ada/SPARK. Rust doesn't so much have a focus on safety and correctness in general, as a focus on memory safety.
Admittedly, Ada/SPARK doesn't make the kinds of guarantees that Rust does about memory. However, accessibility checks help prevent dangling pointers and the use of memory subpools can avoid the need for explicit frees.
Additionally, Ada offers some features like the ability to return a dynamically sized array as if it were on the stack which helps reduce how often memory needs to be manually managed. I believe SPARK may not allow this sort of thing though.
I'm also not sure why you would want to abandon the actually verified properties of Ironsides for a hope those properties remained in an unverified port.
It might add some additional complexity in the first writing of the code, but in return you eliminate whole classes of problems forever. It's not just the initial writing that benefits (at some cost, admittedly), but all future changes won't have those problems either. In the case the types themselves need to change to account for expanded functionality or whatever, you again pay some cost in complexity, but in return every place the new type would cause problems you get a nice error.
The other thing to keep in mind is that whether or not these type are codified in the language they're there conceptually. Just because you have to write them down doesn't necessarily add complexity but is more like forced documentation that can be used to eliminate who classes of problems. It's difficult to see how this wouldn't intrinsically be better than so-called dynamic typing.
I also have tinnitus, but it's nowhere near as bad as yours sounds. Something like this is more than sufficient for me to mask it. It's really only an issue for me when things are very quiet.
Anecdotally, I find it much easier to concentrate with extremely loud music, usually with a strong and at least moderately fast beat. Even if I were to turn this up to 11, I don't think it would help me very much, aside from possibly masking background sounds that might grab my attention. At normal levels, I don't see it making any difference at all.
I almost removed that at the end. I wasn't trying to say much about Rust except that it wasn't predicated on this idea of quickly spinning up new, conceptual types with specific constraints like Ada/SPARK. That sort of thing is really either infused throughout a language, or it isn't used. It doesn't take a great deal of familiarity to see that much.
Actually, just for this response I went and looked into it a little more. Rust has a tiny bit of syntax sugar for creating structs with positional members. So, you can at least wrap things in a struct a little bit easier than in C++, as you don't need to name the internal value. That's really not enough.
Really I mostly wanted to show that Ada also has some means of helping with memory safety - while also being focused on safety/correctness in general. I suppose on that front (and while I'm pushing Ada anyway) I should also mention Ada has a built-in concurrency model, although I suspect you may already be aware of this.
"Ada FOSS community is barely there with biggest deliverables coming from AdaCore."
Yeah, this is the biggest bugbear when it comes to Ada. For what it's worth, there has been some new life on that front and people are working on improving things. So far it's still very, very early days though. The biggest news so far is Gnoga, a web-socket based, uh, web framework that's usable with Gtk WebViews. It will take awhile, but hopefully this trend will continue and the Ada FOSS community will be able to rouse itself.
If you can't tell, I'm not quite ready to count Ada as a lost cause. If it is, and we are looking at running with a new, safe language, at a minimum we shouldn't be forced to take some serious steps back. I'd have loved to see Rust focus on general safety and correctness rather than just memory safety, but it didn't. Losing all that is a rather bitter pill to swallow.
"Ironsides..."
Totally reasonable, and I think it would be very interesting to see.
"Far as Ada vs Rust..."
I've been really hoping to find a good comparison for some time now. I know Rust is able to make stronger guarantees about memory than Ada/SPARK can, but it isn't able to handle every case. I'm really curious to see how well Ada/SPARK is able to handle both what Rust can prove, and what it can't. I also don't know if Rust offers any more imprecise safety nets for the cases it can't prove. Finally, I know nothing about how Rust handles concurrency, so that would be another great comparison to see.
"Note: You should get a real account if you're a programmer AND know Ada/SPARK. Seriously under-represented here."
I might. The plan was for this to be a rather temporary account, but it seems to have stuck.