https://blog.adacore.com/adacore-and-ferrous-systems-joining-forces-to-support-rust
Ferrous Systems is apparently a Rust support company based in Germany.
From the linked page:
"Ferrous Systems and AdaCore are announcing today that they’re
joining forces to develop Ferrocene - a safety-qualified Rust
toolchain, which is aimed at supporting the needs of various
regulated markets, such as automotive, avionics, space, and
railway."
No mention about whether there will be any type of FOSS or community
release. No word on whether the compiler and/or toolchain will be based
on the existing stuff, or something new. Wonder how they will
safety-certify anything in Rust when the language itself doesn't even
have a formal spec. But, it is an interesting development.
Is the writing on the wall for Ada?
https://blog.adacore.com/adacore-and-ferrous-systems-joining-forces-to-support-rust
Ferrous Systems is apparently a Rust support company based in Germany.
From the linked page:
"Ferrous Systems and AdaCore are announcing today that they’re
joining forces to develop Ferrocene - a safety-qualified Rust
toolchain, which is aimed at supporting the needs of various
regulated markets, such as automotive, avionics, space, and
railway."
No mention about whether there will be any type of FOSS or community
release. No word on whether the compiler and/or toolchain will be based
on the existing stuff, or something new. Wonder how they will
safety-certify anything in Rust when the language itself doesn't even
have a formal spec. But, it is an interesting development.
Is the writing on the wall for Ada?
If possible please tell what Rust has to offer over Ada.
From a quick look at the Rust book it seemed weaker in structured programming, generic programming, type system.
Thanks.
Is the writing on the wall for Ada?
I see this going one way, Ada loses out as the Rust side uses AdaCore
to get what they want.
If possible please tell what Rust has to offer over Ada.
From a quick look at the Rust book it seemed weaker in structured programming, generic programming, type system.
Thanks.
But perhaps the company will rebrand itself RustCore :-) ?
Gautier write-only address <gautier_niouzes@hotmail.com> writes:
But perhaps the company will rebrand itself RustCore :-) ?
If the new IDE is called Oxide, watch out ;-).
"Luke A. Guest" <laguest@archeia.com> writes:
I see this going one way, Ada loses out as the Rust side uses AdaCore
to get what they want.
I don't think this is two companies merging. It's two companies working jointly on a particular product. Idk any more than the press release
though.
Regarding Rust vs Ada, I've never heard anything from anyone who is a
real expert at both. Superficially it looks to me like Rust's type
system really is more precise than Ada's in general, although it doesn't
have integer range types. In other stuff like modules, Ada is probably
still ahead.
[Ada vs Rust] Er, try learning both and you'll see?
system really is more precise than Ada's in general, although it doesn'tHow is it?
Ada's ahead in most things.
"Luke A. Guest" <laguest@archeia.com> writes:
[Ada vs Rust] Er, try learning both and you'll see?
It's a big effort to become expert at either, let alone both. Basic or superficial knowledge isn't helpful for such comparisons. I've read
"Ada Distilled" (Ada 95 version) but still have no clue understanding
most of the Ada discussions in this newsgroup, so there is a big gap
between basic and advanced knowledge of Ada.
system really is more precise than Ada's in general, although it doesn'tHow is it?
From what I've heard, Rust's type system is similar to Haskell's.
Haskell's type system can verify stuff just by typechecking, that might
be doable in Ada using SPARK and maybe an external proof assistant, but
not with just types. Example: a red-black tree using Haskell GADT's (Generalized Algebraic Data Types):
https://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/
Ada's ahead in most things.
Idk, I'd like to know more. I've never done anything serious in Ada and nothing at all in Rust, but C++ seems a lot more fluid than Ada, and
Rust is supposed to compare well with C++. C++ of course is terrible in terms of reliability but I'm only referring to the effort needed to bang
out a chunk of code.
You don't need to learn both languages inside and out. You pick a
project and implement it in both languages,
[Ada] Learn the basic part,
[Haskell] So it's no different than a C++ compiler checking against
classes or a variant of C with strong typing?
Still no ranges, subranges, ranges with holes in, etc. This is where
the power is.
Example: a red-black tree using Haskell GADT'sI don't know Haskell. Uni did a shit job at teaching functional, and
logic languages.
1. What do you want to do?
4. Ada is comparable to C++.
4a. Ada > C++ in many ways.
Particularly, a lot of effort in Ada programming goes into making
programs never crash. For example, if the program runs out of memory
during operation it might crash, so Ada programs are often written to
never allocate new memory after a startup phase. In C++ or Rust, it's important not to get wrong answers like 2+2=5, but if your program runs
out of memory and crashes, go get a bigger computer. So idiomatic C++
and Rust programming uses dynamic allocation freely, and that makes some kinds of programming more convenient, at the expense of tolerating
possible crashes.
At uni, we didn't even touch on tagged types, but used controlled
types
"Luke A. Guest" <laguest@archeia.com> writes:
At uni, we didn't even touch on tagged types, but used controlled
types
Of course controlled types are implemented as tagged types. ISTR Dmitry
objecting to this, I think he was right (philosophically; I've no idea
about the practicality of alternate approaches).
If possible please tell what Rust has to offer over Ada.
On 03/02/2022 11:30, Simon Wright wrote:
"Luke A. Guest" <laguest@archeia.com> writes:
At uni, we didn't even touch on tagged types, but used controlled
types
Of course controlled types are implemented as tagged types. ISTR Dmitry
We had a book with a reading guide. We weren't shown the specs showing the type of controlled/limited_controlled. So, when you don't have that information and only know that you can derive from it and then implement 2
or 3 subprograms, you don't need to know about OOP in Ada.
Just like we didn't touch generic packages until much later in the year, generic subprograms, yeah, because u_d was required early on.
objecting to this, I think he was right (philosophically; I've no idea
about the practicality of alternate approaches).
How else would you do controlled types?
Well are you familiar with red-black trees? They are a data structure similar to B-trees which you may have seen. Basically the trees have
nodes that are coloured either red or black, and there are some rules
such as that internal red nodes can have only black children, and that enforces some invariants that keep the trees balanced so that lookups
and updates are guaranteed to run fairly fast.
Now these trees have been implemented in many languages, and if you look
at almost any implementation, there is usually a test suite or internal debugging code to make sure that the invariants are preserved after
doing an update. It is quite easy to make a mistake after all. But the Haskell code doesn't have those tests. Why not? Because the invariants
are enforced by the datatype! If you make a mistake and mess up an invariant, your code won't compile! It's the difference between
checking a subscript at runtime, and verifying that it in range with
SPARK. SPARK lets you get rid of the runtime check. Haskell's type
system is able to do similar things.
In any language with dynamic checks, one can easily reduce the problem
of correctness down to simply proving that no check fails.
So the question is how one can accomplish that with the least
complication for the actual programmer.
Just like we didn't touch generic packages until much later in the year,
generic subprograms, yeah, because u_d was required early on.
objecting to this, I think he was right (philosophically; I've no idea
about the practicality of alternate approaches).
How else would you do controlled types?
Ada 9x originally had a bunch of magic attributes (similar to streaming). It
On 04/02/2022 03:20, Randy Brukardt wrote:
Just like we didn't touch generic packages until much later in the year, >> generic subprograms, yeah, because u_d was required early on.
objecting to this, I think he was right (philosophically; I've no idea >>> about the practicality of alternate approaches).
How else would you do controlled types?
Ada 9x originally had a bunch of magic attributes (similar to streaming). ItNow I want to know what these magic attributes were! Were they specific
to a version of OO? Or were they to enable finalization?
On 02/02/2022 15:29, Marius Amado-Alves wrote:
If possible please tell what Rust has to offer over Ada.
From a quick look at the Rust book it seemed weaker in structured
programming, generic programming, type system.
Thanks.
Don't know why you're asking me, but to me, not a lot, only the borrow checker stuff.
On 04/02/2022 03:20, Randy Brukardt wrote:
Just like we didn't touch generic packages until much later in the year, >>> generic subprograms, yeah, because u_d was required early on.
objecting to this, I think he was right (philosophically; I've no idea >>>> about the practicality of alternate approaches).
How else would you do controlled types?
Ada 9x originally had a bunch of magic attributes (similar to streaming).
It
Now I want to know what these magic attributes were! Were they specific to
a version of OO? Or were they to enable finalization?
If possible please tell what Rust has to offer over Ada.
On Wednesday, February 2, 2022 at 4:29:13 PM UTC+1, amado...@gmail.com wrote:
If possible please tell what Rust has to offer over Ada.
In my minimally informed opinion after going through parts of the official tutorial a couple of times, what Rust has to offer in general:
+ Memory safety (no leaks, double-free, race conditions*) by default.
- Terrible illegible syntax
+ Safer/more expressive/more modern constructs than C
+ Modern tooling shared by all the community
[*] I guess in a protected-object sense, not in a high-level logic sense. But I don't really know.
The thing is that C is so basic and C++ so prone to shooting yourself in the foot, that Rust hits a middle ground that feels
like the best thing since sliced bread to C/C++ programmers wishing for something better. Add to that the true novel contribution to a mainstream language that is memory safety (this is really a new way of thinking when you get into Rust), that if youdon't know better (e.g., Ada) it really is overwhelmingly compelling. I'm not surprised at the cult-like following (I mean, we feel like that sometimes in the Ada world, right?) In a sense, Rust is the Ada of a younger generation, and without the baggage.
Of course you sometimes have to use "unsafe" programming evading the borrow checker, just like pointers are sometimes a necessity in Ada; and the legibility becomes truly awful IMHO really fast (to me, this is THE Achilles heel nobody seems to care toomuch about), but as I said, it has a couple of real selling points over the competition. Of course, if legibility is not your concern because you're used to C++ templating nightmares, you don't feel that particular pain. It's always the same story with
The whole memory safety thing with the borrow checker goes beyond a gimmick, and it has a solid quality which goes beyond "in Ada you don't need pointers most of the time". It's a compile-time check, and it makes evident that runtime checks are a poorsubstitute.
I'm more ashamed now of the whole anonymous pointers and accessibility surprises in Ada.
Yes, SPARK added something similar for pointers, but in Rust it is for all variables. The equivalence in Ada would be not being able to use the same variable in two consecutive calls as an in-out parameter. So it's not the same, besides being only inSPARK.
Not having done anything of real import, I'm not sure how inevitable it is to go unsafe in Rust. My guess is that it will be hidden in libraries just like the Ada standard containers contain some scary pointer use (and I mean that I wouldn't like tohave to understand what is going there with the tampering checks etc.) At that point, obviously, you've lost the most solid selling point IMHO. Ada is safer not in a single sense, but as a whole design.
All in all, Rust has one big thing that Ada hasn't, which is the borrow checker.
And that is what how I would summarize it: Rust is better in a single narrow sense, but Ada is better as a general language. Which is, not surprisingly, the consequence of the design motivations for each, which were precisely to have a memory-safelanguage and a high-integrity-oriented language. So the funny thing is that both have succeeded at their objective.
I really miss not having the time to become proficient in Rust at least to be able to properly compare. I think the memory safety is great to have (and if Ada were designed today, I guess it should play the same integral part, if practical), but Rustis demanding on the programmer in a way that C/C++ aren't, and the maintainability seems suspect, so I don't know how far it will carry Rust into the future. I guess it could absorb a big part of both new C and C++ development.
Boy, can I write a lot sometimes...
I really miss not having the time to become proficient in Rust at least to be able to properly compare.
In my minimally informed opinion after going through parts of the official tutorial a couple of times, what Rust has to offer in general:
+ Memory safety (no leaks, double-free, race conditions*) by default.
...
[*] I guess in a protected-object sense, not in a high-level logic sense. But I don't really know.
In a sense, Rust is the Ada of a younger generation, and without the baggage.
Of course you sometimes have to use "unsafe" programming evading the borrow checker, just like pointers are sometimes a necessity in Ada...
and the legibility becomes truly awful IMHO really fast (to me, this is THE Achilles heel nobody seems to care too much about
The whole memory safety thing with the borrow checker goes beyond a gimmick, and it has a solid quality which goes beyond "in Ada you don't need pointers most of the time". It's a compile-time check, and it makes evident that runtime checks are a poorsubstitute.
I'm more ashamed now of the whole anonymous pointers and accessibility surprises in Ada. Yes, SPARK added something similar for pointers, but in Rust it is for all variables. The equivalence in Ada would be not being able to use the same variable intwo consecutive calls as an in-out parameter. So it's not the same, besides being only in SPARK.
Not having done anything of real import, I'm not sure how inevitable it is to go unsafe in Rust.
And that is what how I would summarize it: Rust is better in a single narrow sense, but Ada is better as a general language.
Rust is demanding on the programmer in a way that C/C++ aren't...
Agree too, but only because they use K&R style. I find Allman style quite readable.and the legibility becomes truly awful IMHO really fast (to me, this is THE Achilles heel nobody seems to care too much aboutI agree with this. It's not as bad as C++, not even as bad as C IMHO, but the braces get old. If not for IDEs that can help navigate them, I'd get lost pretty easily.
So, you'd prefer, if Ada was designed now, it didn't do runtime check(on pointers) and have compile-time checks?
I'm more ashamed now of the whole anonymous pointers andaccessibility surprises in Ada.
Here's what Rust promises: https://doc.rust-lang.org/nomicon/races.htmlprogram to get deadlocked or do something nonsensical with incorrect synchronization. ... Still, a race condition can't violate memory safety in a Rust program on its own."
"Safe Rust guarantees an absence of data races, which are defined as... [omitted] Rust does not prevent general race conditions. This is pretty fundamentally impossible, and probably honestly undesirable. ... So it's perfectly "fine" for a Safe Rust
I agree with this. It's not as bad as C++, not even as bad as C IMHO, but the braces get old. If not for IDEs that can help navigate them, I'd get lost pretty easily.
two consecutive calls as an in-out parameter. So it's not the same, besides being only in SPARK.I'm more ashamed now of the whole anonymous pointers and accessibility surprises in Ada. Yes, SPARK added something similar for pointers, but in Rust it is for all variables. The equivalence in Ada would be not being able to use the same variable in
Maybe I misunderstand, but I think the analogy's incorrect. When you designate a Rust variable as mutable, you can in fact have two consecutive calls in a manner akin to "in out", _so long as_ the function declares it wants to "borrow" the variable asmutable, *and* so long as the caller gives permission for both the borrow and the mutability. If it doesn't, the compiler gives a very clear error message.
I'm not sure Ada has anything comparable to that.
At work we have a fairly non-trivial Rust system that, as far as I know, goes unsafe only when... you can fill in the blank. :-)
And that is what how I would summarize it: Rust is better in a single narrow sense, but Ada is better as a general language.
I haven't played with Ada's task & rendezvous mechanisms in a long time. Do they guarantee an absence of data races?
If not, I'd say that's something else Rust has that Ada doesn't. I think SPARK does guarantee that, though. (If I understand correctly, the key is to disallow mutable objects being passed to multiple tasks / threads / etc.)
Rust is demanding on the programmer in a way that C/C++ aren't...
Perhaps, C/C++ are demanding on the programmer in all kinds of ways that Rust isn't, and none of those ways is good. ;-) Whereas Rust's demands are pretty much all good (in comparison to C/C++).
I would also add that Rust has an amazing and effective ecosystem of libraries that are extremely easy to download and build, all as part of the generally-used Cargo build tool,
I have the impression that alire is inspired by Cargo, but I haven't used alire at all yet, so I don't know how it compares beyond the ability to create projects and download libraries.
I also don't know if alire is nearly as comprehensive as what Cargo offers [...] alire has about 220 crates).
I have a feeling that abundance of crates, and the ease of incorporating and using them, has at least as much appeal as the guarantees on any safe code you may write.
I agree here. Rust prevents misuse of global variables at the low level
of simultaneous access (from what you referenced before). This certainly
can be useful in refactorings going from a single- to a multi-threaded design. In Ada you'd have to inspect every package for global state.
SPARK deals with that, of course, but again: not Ada.
On 12/2/22 6:22, John Perry wrote:...
I haven't played with Ada's task & rendezvous mechanisms in a long time.
Do they guarantee an absence of data races?
Not for global variables, yes for task-local ones. For any decent design you'd encapsulate any shared data in a protected object or task, which
would give the same assurance as the bit you quoted for Rust. Then there's Pragma Detect_Blocking, but that will only work for protected operations,
and two tasks getting in a mutual deadlock needs not to involve protected operations.
It doesn't prevent every data race, but it eliminates most of
them. (You can still get in trouble with accesses to multiple objects;
that isn't necessarily safe even if accesses to the individual objects
are.)
If possible please tell what Rust has to offer over Ada.
From a quick look at the Rust book it seemed weaker in structured programming, generic programming, type system.
Thanks.
On 02/02/2022 15:29, Marius Amado-Alves wrote:
If possible please tell what Rust has to offer over Ada.
From a quick look at the Rust book it seemed weaker in structured
programming, generic programming, type system.
Thanks.
Don't know why you're asking me, but to me, not a lot, only the borrow checker stuff.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 307 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 102:56:02 |
| Calls: | 6,851 |
| Calls today: | 2 |
| Files: | 12,355 |
| Messages: | 5,415,473 |