To be fair, this is not the entirety of C++ but C++ following the Google C++ Style Guide, which limits use to a more manageable subset of the language. For instance, exceptions, which can be especially hairy in a language with manual memory management, is prohibited. Take a look at the Fuchsia codebase. The code is really quite clean and readable.

Random muse, but God damn I love Google's code quality.

Compared to the midnight bamboo forest my company built. A challenging codebase, not by its merits but because you need to be clever just to find your way through.

Anyone know if Google is hiring webforms developers?

  Why do you want to implement something small with
  something that is large?

Consider the size and amount of equipment involved in making watches. Or microchips, for that matter.

Do you carry that watch-making equipment on your wrist along with your watch?

Of course not. I only need them in my workshop/foundry/dev machine.

>C++. Oh lord. Why are you writing a microkernel in C++? If there was anything they learned from L4 (Xen, Linux, ...) it is that C is sufficient. Why do you want to implement something small with something that is large? This one is a real head scratcher.

Because if there was anything proven from years and years of using C, it's that it is woefully insecure and should not be trusted to write a kernel with.

You can still fuck up with C++, sure, but std::shared_ptr offers more guarantees than *.

EDIT: HN stop eating my stars

Yes, we know that C is not secure. We also know that C++ is not secure and moreover it definitely isn't C, now with security. It's just more bigger C. So use your phrase, you can still fuck up with C++. You can just do it in more clever and insidious ways.

seL4, a third-generation microkernel is 8,700 lines of C code and 600 lines of assembler.

http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4....

So we also empirically know that you can formally verify a microkernel written in C. Now if the Fuchsia folks had gone ahead and formally verified their microkernel, this issue would be moot. But they haven't. So we are instead left with std::shared_ptr offers more guarantees than *. While this isn't nothing, it isn't much either.

I wouldn't use SEL4 as an argument. It is completely unreasonable to build a production kernel the way they did - it took them ages to get what they had. Google is probably looking to develop features/ move code a lot faster than is possible using their technique.

Good coding practices take no time to implement, you learn it once and you write that way. It is not bullet proof, neither are capabilities. Still, at least they're practical.

I think you miss the point of a microkernel! The point is to keep all your "features" outside of it, and to use it only to implement the core set of functionality necessary to have secure shared access to the hardware. The general L4 concept has proven industry use, so there's no reason you can't take advantage of the already accomplished work on seL4 to bootstrap your own secure OS.

It's true that seL4 is not a magic safety or security bullet; in particular, their FAQ says that they haven't completed extending their proofs to DMA safety via VT-d or SystemMMU on ARM, so DMA-accessing services would have to be separately verified. And its particular feature set may not be appropriate for all situations. But if its API does work for you, it would be foolish not to at least consider using it.

It is really unreasonable to dismiss seL4 simply because it took them a lot of effort to create it. That effort is now done and can be re-used and magnified by further effort.

I didn't realize you were recommending to use sel4, I assumed you meant they should have proven theirs using similar methods.

How about Muen separation kernel in SPARK Ada with automated prover eliminating many classes of undefined behavior? Or C with tools like Frama-C and Astree Analyzer (like SPARK for C)? C++ can't reach the safety of its competition due to more complexity and less tooling.

To be fair, if Frama-C is an option, as someone on the C++ side of the fence (C vs C++) I would advocate High Integrity C++ is also an option. :)

http://www.ldra.com/en/software-quality-test-tools/group/by-...

I thought about it. The reason I left it off is a lack of static analysis, automatic generation of tests, certified compilers, etc. There's tons of FOSS and commercial vendors for doing such things in C with quite a bit for Ada. Whereas, I could find only one or two products for C++ that seemed like it would be really helpful as opposed to just kind of. So, I pivoted my recommendations to go with languages that have huge, tooling ecosystems in academic R&D and commercial. You can certainly use it but might get less value in long term.

Embedded, real-time Java could also be on the list since Java ecosystem has a verification tool for about everything. CompSci loves Java for some reason (probably mandated classes). Yet, verifiable C and SPARK are closer to the metal than embedded Java plus no Oracle risk. So, left off Java as well.

I guess so, I just know it from reading about it, so it might be that when using it won't be as suitable as I think it could be.

On the Java side you can probably check what Aonix used to do, they are now part of PTC.

http://www.ptc.com/developer-tools/perc

Also there are the guys from MicroEJ.

http://www.microej.com/products/device-software-development/...

There is no Oracle risk with Java, when companies play by the rules.

PTC, Aicas, IBM, MicroEJ, Excelcior JET, HP, Cisco, Ricoh, Azul, Red Hat and so many other companies are selling JDKs with their own set of features, without having had any issue with Sun or Oracle.

Only Google has an issue with Oracle, because they decided they were the cool kid better than anyone else whose rules don't apply to.

I'm only commenting on seL4's approach not being very viable. I'm not advocating for C++ in the kernel either.

Fair enough.

"folks it's ok, we're using shared_ptr's. We're safe. Problem solved."

Shared_ptr is slow. It has an atomic variable for reference counter - it is supposed to be thread safe...