>>54976671

>A formal proof of functional correctness was completed in 2009.[15] The proof provides a guarantee that the kernel's implementation is correct against its specification, and implies that it is free of implementation bugs such as deadlocks, livelocks, buffer overflows, arithmetic exceptions or use of uninitialised variables. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified.

Nice, but the again it's a micro kernel

>>54976729
And so?
>muh performance
L4 was designed with performance in mind too.

You misspelled FreeBSD.

>>54976850
You misspelled monolithic ancient shit

>>54976850
>Free vulneraBilitieSD

>>54976850
>tried BSD in vmware
>installed vmware related shit
>nothing worked
FreeBSD, not even once.

>>54976899
>VMware
Found the problem!

>>54976881

Reminder that Linux has 0 mitigations.

>>54976877

Microkernels are to OSs what functional languages are to programming: edgy memes pushed by academia with no real use.

>>54976850
You misspelled misspelt.

>>54976925
>no use
Normies use L4 for protect their shitty iPhones.
L4 is deployed in routers and shit. Same with QNX.
The fact that Mach was a massively over enginnered piece of shit and everyone remembers that doesn't exclude that microkernels are useful and more robust that monolithic pieces of shit.

>>54976941

Miss Pelt*

>>54976910
But the problem was FreeBSD

>>54977192

VMware is pajeet-tier proprietary garbage. You may not post in this ITT thread if you don't poo in the loo.

>>54977210
>tried BSD in Virtualbox
>installed Virtualbox related shit
>nothing worked
Can confirm that FreeBSD also doesn't work on Virtualbox.

Almost every microkernel design has become progressively more monolithic through each iteration.

Purity in design always loses to pragmatism, at least outside of academia, where novelty is the goal.

>>54976729

SeL4 is an interesting case study, but it's single-core only, which sadly will seriously limit its use cases.

They're working on a multi-core version, but it works by dividing the entire machine up (eg if you have a quad-core, you get 4 independent single-core OS instances which each get 1/4 the system's ram).

>>54979077
>but it's single-core only, which sadly will seriously limit its use cases
That doesn't sound like it will be an issue if you're using it for an embedded system (like a router or industrial equipment).

>>54979109
>virtualbox is shit garbage
I've never had any issues with it, besides that one time that I tried to run it in a liveCD as a non-root user.

>>54977250
>installed freeBSD on my pc
>installed pc releated shit
>nothing worked
can confirm that freebsd also doesnt work on baremetal