1. 51
  1. 10

    Check out QBE on the topic of an intermediate language that’s easier to verify. It’s designed to be a more understandable compiler.

    Far as testing, CompCert got qualified. Many academics already target Clight to reuse its proofs. Rust front-end targeting it might reuse part of its certification package. Solid Sands was doing the test suite last I read.

    1. 6

      Hey everyone, this is a very high-level post and it sums up a lot of conversations that we mostly had in private. If there’s any questions about specifics, we’re very happy to answer them and go in a little more detail!

      1. 6

        How is the FIPS problem addressed? That is, the problem that bugs get certified so fixing bugs would invalidate certification.

        1. 5

          I think the straight and upfront answer here is: currently not at all. We’re not at a stage where enough people sit at a table to competently discuss it and giving an answer would be hard for me individually.

        2. 1

          [getting contact with] Companies interested in using [sealed rust]

          I’d be curious how many companies have contacted you. My pessimistic view doesn’t expect many companies in that environment to be interested in adopting something new. Having to throw existing codebases away or investing into something when it’s at that of an early stage. So I’m curious about this.

          1. 7

            I can only be hand-wavy around this, because most of these meetings are private. But we have talked to some companies in each industry except avionics, both suppliers and product companies, both on the hardware and software side.

            Every larger tech company in that space plans from 5 to 50 years ahead (depending on their business and support cycles) and have specific departments responsible for that. The way they grade projects is where they move. Some have tracked Rust over the last years and gave good feedback that the project is moving in the right direction. One produced their evaluation and it turned out that they re-evaluated every year and figured out if Rust is moving their direction (it does).

            Every company of a certain size is taking long bets and is aware that any technology that is going to feasibly replace their current stack will be in an early stage at some point. The Sealed Rust effort is a vehicle to convince people that this long bet is the right one.

            Having to throw existing codebases away or investing into something when it’s at that of an early stage.

            Indeed, the strong pitch of Rust is (contrary to public memes) is that you don’t have to rewrite everything in Rust, but that the language integrates well with existing projects and augments them. You can write Rust on C-based RTOS like RIOT today. And there’s good reasons you should! I was at the hackfest where they enabled that, it took them ~1.5 hours.

            The possibility of gradual adoption and a track record of large projects that did that (e.g. Firefox) is a very strong argument for management.

            Finally, there’s a wind shift: LLVM is becoming a considered alternative at many places and moving of vendor-locked in toolchains becomes less and less an interest of clients. Rust not being owned by a company is a strong sell.

            1. 1

              Who in these companies is interested?

              I’m employed by large automotive company which (imho) should be interested in Sealed Rust but I have no clue how to push it. Should I contact some high-level manager? Researchers? People involved in standardization gremiums? Rust fans? Which kind of departments? Any other patterns?

              1. 1

                As above, I can only hand wave. This is a bit annoying to me, as I’m usually used to publicly communicate as much as possible. So these posts are our way of trying to at least transpire some of our learnings.

                But on your topic: companies should be interested in Rust first, Sealed Rust comes after it - it’s the reassurance that their concerns have a place.

                There’s multiple ways to start gathering interest, but there’s a prime directive: don’t annoy people and make sure that you always argue from a stance of companies best interest. There’s the marketing sentence “only speak to people in pain”. If someone is happy with something and it currently works for them, there’s no point in talking. Resarchers are no bad contact either, they should be curious at heart. Standardisation people are rarely interested professionally. I can’t give a good recommendation there, except that I would try a couple of people and ask questions like “would you know someone who might be interested in this?”. I always describe this process as “mapping out the space”. Done appropriately, it’s also a great way to get to know new parts of your company :).

                But still be self-confident that the thing you are proposing is good. Generally: Making your interests known has never caused harm. That might make the conversation come to you - someone approaching you out of curiosity is a much better then trying to kickstart a conversation. For example, if you have an internal channel where people share general tech news, share news like the post above there. That’s has been a big driver for Rust and Sealed Rust in general, conversations in those general tech spaces.

                On the Rust fans: seek them out and try engaging with them. Many companies that I know adopting Rust started out with an internal #rust channel on slack ;).

                Finally: ignore the naysayers. They just waste your time and energy. Don’t get into fights. Speak to people that want to discuss the subject.

                1. 1

                  There is a chicken and egg problem:

                  companies should be interested in Rust first, Sealed Rust comes after it

                  How can a company building safety critical stuff be interested in Rust without a Sealed Rust? Last week I saw a presentation where they dismissed Ada for lack of ASIL qualification.

                  1. 1

                    Because interest predates adoption. Sealed Rust not being implemented is not mandatory for interest. It is mandatory for adoption. Convinced companies are willing to invest in future solutions. And indeed, a lot of the discussions ran along those lines.

                    There are presentations around for every viewpoint, but these are just that: viewpoints. In a company of over 1000 employees, you’ll probably find all viewpoints.

                    The point here is: If Rust is not at all fitting the bill, there’s no amount of additional work that can help that. “Rust would be interesting if it provided $X” is the moment where Sealed Rust comes in.

                    Also, be aware that a lot of people, especially in IT, only conceptualise the present. You want to speak to people that conceptualise the future.

        3. 3

          This is great. Some people like to criticize that rust doesn’t have “a specification”, which this should fix (a normative spec, that is). And using rust for high-quality, high-assurance software seems like a great fit anyway. I’ll be curious to follow this effort.