sel4 seems to be the most robust and active microkernel OS out there. how come it isn't more used and talked about? am i missing some drama?
>>101559600It doesn't look like there are any operating systems using it, I'd have to do everything myself.
>>101559600I think it would be much better received here if the seL4 dev went to live in the woods and mailed out some pipe bombs to people. Or at least went on some schizophrenia-induced rants about CIA and then got hit by a train.
an OS for computer controlled machinery isn't necessarily suited to sending email and browsing the internet
>>101559600how is it better than sel3 and sel2?
>>101560303It's like some companies don't even care about marketing anymore.
>>101559600Isn't it impossible to get it to run on a vm without having a phd? I don't think they even offer binaries.It's not one of the most used microkernels by far, Minix or Mach are much easier to run on a PC.
>>101559600Is this the one with a full proof of correctness?
>>101559600redpill me on it, I remember seeing somewhere there was a linux distro that used something like this. In terms of why it's not popular, its likely the same problem Plan 9 and *BSD systems have where they may in theory be a better designed system, but the anons on this board have a limit to their autism and won't use something beyond the linux kernel if their CPU isn't even guaranteed to work with it.
>>101563721>requires phd to run on a vmi played around with camkes couple years ago and i'm a highschool dropoutjust rtfm, chromosome hoarder
>>101559600>how come it isn't more used and talked about?too technical for /g/
>relies on a verification toolchain that accepts phase-2 UBs>single core>zero applications>abysmal documentation>devs actively hostile to POSIXretarded bait for college students
>>101566759>>devs actively hostile to POSIXAs they should be, if they care about security.
>>101566851What's insecure about user permissions?
>>101566759BASED
>>101564697Hmm. Ok, fair enough.But the insult was unwarranted.
>>101566759>relies on a verification toolchain that accepts phase-2 UBsBy that you mean the proofs accept undefined behavior for some inputs? Where are you getting that from?
>>101560411There is no seL2/seL3. >>101564629nto. seL4 is a from scratch microkernel inspired by and based on L4 which was a continuation/reimplementatiom of L3 (it's the first iteration). L3 and Mach were some of the first microkernels to exist and showed off its capabilities and advantages over monolithic kernels. seL4 apparently is also end to end verified with a focus on security (https://trustworthy.systems/projects/OLD/l4.verified/home.pml/)>>101559600Off the top of my head, I really only knew about KataOS (likely part of the Google graveyard now) and Robigalia OS. Plus they only seem to care for ARM and Risc-V at the moment. They only seem to care for embedded markets and barely have drivers. Apparently they want to make a toolkit for making OS called MicroKit and a reference OS called LionsOS (https://docs.sel4.systems/projects/roadmap.html/).Here's a list of projects I found on their website: https://docs.sel4.systems/CommunityProjects.htmlHere's another website: https://www.osrtos.com/rtos/sel4/
