And yet your post can be summarized as "I am not aware of the usage of L4 microkernels".
>The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied...
Except their "other demands" are satisfied. It implements L4, just like every other L4 implementation does. It also happens to be the fastest L4 implementation ever tested. So rather than vague dismissive "calling BS", how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead?
>how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead?
I'm talking about people in general, prefaring their mainstream OS of choice over some platform based on L4.
Not about L4 users opting for this or that implementation.
The parent talked about people in general not caring for software quality, while those L4 users are highly specialized enteprises and businesses making a choice.
My post said nothing of the sort. Trying to justify your shitposting by saying I am to blame for your assumptions is ridiculous. If you don't know about the subject, don't post about it as if you are an authority.
And yet your post can be summarized as "I am not aware of the usage of L4 microkernels".
>The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied...
Except their "other demands" are satisfied. It implements L4, just like every other L4 implementation does. It also happens to be the fastest L4 implementation ever tested. So rather than vague dismissive "calling BS", how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead?