I am surprised they didn't mention Iris[1] and RustBelt[2] projects. Iris works on creating the formalization framework based on separation logic and Coq. They have the Rust code model specifically[3].
Sealed Rust Update
11–20 of 34 posts
Re: Sealed Rust Update
#12I don't get why there is so much love for Rust but so little love for Ada?
There's plenty of love for Ada, more than ever.
Re: Sealed Rust Update
#13I don't get why there is so much love for Rust but so little love for Ada?
Potentially interestingly, it looks like there's ongoing work to get Ada compiling to wasm via LLVM too.
Hello World style demo:
https://blog.adacore.com/use-of-gnat-llvm-to-translate-ada-a...
Re: Sealed Rust Update
#14This is an important effort, but it's weird (disconcerting?) to me that something so fundamental as a formal language specification (for a language that advertises safety as a key feature) is being bootstrapped not by the core team, but by a third party. It doesn't feel like that's something you only need "collaboration with" the core team about. I can't think of anything that's more "core". The rest of it makes sens…
Speaking bluntly:
Almost everyone using the language at present is getting by just fine without this. As a normal Rust developer, I don’t particularly care about a formal language specification existing. It’s a long way down my list of nice-to-haves—yeah, it would be nice to have, but there are quite a few other things that would be more nice to have.
The core team are compiler and language developers. I’d much rather have them working on the language, rather than a formalisation of the language that isn’t going to benefit me particularly for many years. If there are other people that are interested in doing that work, good on ’em; it’ll be interesting to see what happens, but I don’t want the core developers distracted with this sort of speculative work—for this is a heavily experimental area. This is absolutely a place for only a collaboration, rather than having it being managed by the core team. If the core team were focusing on this, everything would collapse in a heap. The core team is a very finite resource that does not specialise in this sort of thing in any way.
Re: Sealed Rust Update
#15I want much more runtime performance out of rust more than anything else. Faster builds are second on the list. This probably doesn't even make top 10. Who is this aimed at? And I would hate for those top goals to be subverted for this.
From the previous blog post ("Part 1: The Pitch"[1]): > We hope that the Sealed Rust effort would be applicable to any developers working in safety critical software domains, such as: > Automotive (under safety standard ISO26262) > Industrial (under safety standard IEC61508) > Robotics (under a number of safety standards deriving from IEC61508) > Medical Devices (under safety standard IEC62304) > Avionics (under safe…
I work in medical devices and out-of-the-box rust would be a much better option than the C++ systems we build!
There is competition in this space from qnx as well.
Take a look at the medical device alarms standard IEC 60601-1-8. It's possible to provide a very generic implementation of the standard for high, low and medium priority alarms. Could act as a trojan horse to introduce your back end messaging, logging, shared memory infrastructure - all developed according to ISO 62304 (of course)!
Re: Sealed Rust Update
#16I don't get why there is so much love for Rust but so little love for Ada?
I guess, due to a couple of things.
1 - There is a younger generation that thinks C and C++ are the only game in town, and never learn about myriad of systems programming languages going back to 1961.
2 - This same generation is very averse paying for tooling and among the six surviving Ada compiler vendors, GNAT is the only free one, and even then discussions about its licensing pop up ('cause lets have free beer)
3 - Ada suffers from the whole bondage vs cowboy programming theme that was so common in the early 90's. Where many could not grasp the benefits of type driven programming.
4 - You need a strong engineering background, specially on high integrity computing domain, to understand why Ada offers what it does
6 - Due to high integrity computing domain, Ada tends to be used in domains that many don't find cool, government contracts, train control systems, airplane avionics, pages long contracts with project management very waterfall like even when they pretend to be agile now
7 - It is definitely not a language for the Silicon Valley culture.
However thanks to Ada being there first, having the certified compilers, being deployed into production during the last 40 years, with the increasing number of security exploits, some companies have been adopting Ada, NVidia being one of them.
https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-auto...
Two of the reasons, for why Ada and not Rust, was precisely the lack of maturity of Rust on high integrity computing and Ada being more approachable to their engineers. They did a webinar about the adoption process.
Re: Sealed Rust Update
#17I don't get why there is so much love for Rust but so little love for Ada?
Did Ada - or rather its proponents - make any effort to get people to learn it? If I google for "Ada programming language" I do not even find what could be an official site? I thought it could be adacore.com, but that's a commercial offering. Wiki tells me it could also be adaic.org, which errors out with "SSL_ERROR_UNSUPPORTED_VERSION" in current Firefox. Even if I could access the site: Would I find tutorials? Other supporting material? Explanations why I should use Ada?
If you want people to use your language you have a to put in work. Even more for a language with the reputation of Ada (the sibling comment by pjmlp gives a good overview).
Re: Sealed Rust Update
#18I don't get why there is so much love for Rust but so little love for Ada?
Ada is not cool. More seriously, GNAT crashed all the time in random ways when I tried it, and when I tried adacore on stm32, the timing functions were based on systick, that’s a non-starter for me, and I didn’t want to start learning a new system by re-implementing part of its internals.
Re: Sealed Rust Update
#19This is an important effort, but it's weird (disconcerting?) to me that something so fundamental as a formal language specification (for a language that advertises safety as a key feature) is being bootstrapped not by the core team, but by a third party. It doesn't feel like that's something you only need "collaboration with" the core team about. I can't think of anything that's more "core". The rest of it makes sens…
Speaking bluntly: Almost everyone using the language at present is getting by just fine without this. As a normal Rust developer, I don’t particularly care about a formal language specification existing. It’s a long way down my list of nice-to-haves—yeah, it would be nice to have, but there are quite a few other things that would be more nice to have. The core team are compiler and language developers. I’d much rathe…
I think the argument is that if you said that about C++ everyone would be "yeah: this is just a useful tool, so why do I care?"... but Rust is about safety, and if you don't have a formal model of the language by what reasoning could you possibly have to know it is safe? (And, in fact, every now and then--much less often these days, but still--someone finds a soundness issue in Rust itself, something you would hope to have been able to disprove at the outset using a proof over a formal model.)
Re: Sealed Rust Update
#20I don't get why there is so much love for Rust but so little love for Ada?
Getting started with Ada is hard. The best compilers and runtime for it are commercial, and especially getting it to work in embedded (where it really shines) is not at all straightforward. I've looked at it a few times and never really been able to get anywhere useful with it, and came away with the impression the best way is to drop a few thousand on it or work on a government contract.