Redox – A Unix-Like Operating System Written in Rust

There is this comment :) ..

    /// Into a cow
    pub fn into_cow(self) -> CowUrl {
        /*
             ______________
            
             --------------
                    \   ^__^
                     \  (oo)\_______
                        (__)\       )\/\
                            ||----w |
                            ||     ||
         */
        CowUrl::Owned(self)
    }

The self-healing in Windows' graphics system is pretty awesome and very practical. Also what does 'not perform well' mean? Not well enough for what?

  > Lack of bitfield support and lack of a "restrict" keyword 

https://crates.io/crates/bitflags

Rust automatically adds the appropriate 'restrict' annotations to `&mut T` pointers, or well, does generally, but I think an LLVM bug made us take it off temporarily. Point is, this isn't something that you annotate in Rust like you do in C, you use the type system and the compiler handles it where appropriate. (It's more than just &mut T, like, UnsafeCell will also cause the annotation to _not_ happen, for example.)

"My understanding is that Rust doesn't have so much to offer Ada/SPARK. I haven't looked that hard at Rust though, so maybe I've overlooked some of it's features."

I liked the juxtaposition of that haha. It kind of negates anything about Rust in your counterpoint. Your points on Ada/SPARK are still worthwhile.

"Ada offers..."

No doubt. It was systematically designed to reduce the existence or impact of flaws throughout software. They kept this up in extensions. SPARK straight up proves the absence of them in a subset. So, it's what my gold standard is for safe, systems programming. Rust is the newcomer with interesting additions inspired by safer-than-C imperative and functional languages. It's confusing scheme for memory and concurrency protection is said to be quite effective. It might end up better than Ada over time or just different tradeoffs. The important thing, though, is that it has what Ada/SPARK will likely never have: large-scale adoption with uptake by big companies and users who will add to its ecosystem. Ada FOSS community is barely there with biggest deliverables coming from AdaCore.

Remember Gabriel's Worse is Better? Real lesson of it is certain things get adoption better than others. Best to bet on them. Rust is in that category a bit but with Right Thing elements. So, it's worth investing in for long-term benefit of IT.

"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."

I'm not necessarily suggesting that. There's a reason that OpenBSD and some proprietary vendors keep their system working on several compilers. There's a reason NASA project here used 4 static analysis tools. There's a reason B3/A1 systems kept detailed, formal specs side-by-side with code with both checked. The reason is that different tools catch different types of problems. Further, a problem detected in one might apply to the other. Now, a semantic difference exists between Ada/SPARK and Rust. Yet, there's usually a subset and/or style one can use where results from one about memory or control issues will apply to the other.

So, I said do it in parallel: both Ada/SPARK mix and Rust. It displays how each language handles the problem. It let's the analysis tools of each check it for problems that might exist in both. Tool version of many eyeballs except works consistently. ;) It also means that compiler optimization problems in one might not affect an other. Can help with hotfixes while compiler team develops guidance or patches. Also, provides two implementations that can help with adoption and support. There's an issue of maintaining parity but the simpler version is write it in Ada/SPARK w/ Rust release getting uptake.

That's the lines I was thinking on. Rust is popular and better than usual. Ada is equal or better in capabilities but not going anywhere. Leverage both to get benefits of both maybe defaulting on Rust release for adoption. Far as Ada vs Rust, I'd like a less biased party that knows Rust's protections and features through and through to do a comparison for me. I have a reference listing each issue Ada tackles and how. I probably can dig up one for SPARK 2014, too. I would love to see what mainstream answer to Ada can do vs the baseline it created.

Note: You should get a real account if you're a programmer AND know Ada/SPARK. Seriously under-represented here.

Good work. Not quite an OS like what they're trying to build, though. I've always thought these discussions could benefit from different categories of OS like single vs multi-user, UNIX-like vs non, embedded vs desktop vs server, local vs distributed, and so on. A soft-real-time, single-user OS is much easier to write than a UNIX alternative that's similar in capabilities. So, one can certainly write a RTOS more easily than many applications on servers or desktops but the statement seems apples to oranges applied to mainstream perception of OS's (aka desktops, servers, or iOS/Android).

"The joy I get out of doing it again vastly outweighs the pain of writing HTML by hand, but barely :-)."

Haha. I can't talk given how disorganized my stuff is. Hell, I don't even have a blog: I have text files and PDF's I send to people that ask. Gopher is on another level compared to how I do things.

Nonetheless, it's good to know people that did embedded systems as I'm slowly accumulating knowledge on that sort of thing in my exploration of secure hardware/software systems. Really wish I spent more time on embedded and HDL's back when my brain worked reliably. That's where best bang-for-buck in security and reliability are. The more people write openly on such topics the better. So, consider organizing anything you have on the magic you used to do stuff like that web server.

Side note. I'm peripherally gaining information on doing 8- or 16-bit software for microcontrollers. Hell, I even have some docs (and maybe HDL source) on a 1-bitter although with 8-bit ALU. Do you have any resources I can give to new people showing the tricks people use to reliably do complex or fast stuff with them? SymbOS would probably be high-end of that but I intend to use them in peripheral controllers, monitoring, and such.