SeL4 gets formal verification on x64

All you need to do is port glibc to SLE4. There is hardly any other code in GNU that specifically relies on Linux.

Yeah take this great very well designed formally verified system and port this massive pile of horribly bloated shit on top

t. guy who understands fuck all about how the OS his programs run on works

You also have to implement all the things glibc interfaces with, which is 99% of the work. seL4 only gives you scheduling, memory management, and IPC, everything else has no business being in kernel space and so isn't implemented.

Pic related doesn't even begin to convey the complexity of modern Linux/glibc.

Attached: Linux_kernel_System_Call_Interface_and_glibc.svg.png (1440x1080, 439.65K)

You know what I do not appreciate about glibc? The feature macros. It's unnecessary. If I am writing a program that uses strcasestr, it doesn't matter if it's compatible with any other program but the call to strcasestr. GNU/FSF etc. do this to make software developers forced into a situation to license their software with the GPL. It's garbage. I can write and have written a strcasestr function that doesn't need shitty GNU software.

I hope for a day that the only GPL'd software in a Linux is the kernel itself, and I hope that that day will lead to the Linux kernel to being relicensed to something that is not GPL.

Is there anything more obnoxious?

GPL restricts your freedom.

AFAIK Linux does not require contributors to transfer copyright to Linus or the Linux Foundation, so there are tons of issues with relicensing. Each contributor with code in the kernel would have to be tracked down and would have to agree to the change. Or their portion of the code would have to be rewritten, probably in a clean-room manner.

You could fork the kernel and wait for all of what was written up to your fork become public domain. That'll probably be in the mid-2100s, depending on how long Linus and the other contributors live. Take your statins.

You can't throw out old software every few years and expect to stay relevant.
Serious backwards compatibility is one of the things that make Windows the only usable Os for most people.

Quite a few functions and macros in the Linux kernel are licensed under the GPL for the same reason, to force developers of kernel modules to license their code under the GPL. Insidiously many aren't, its only the more useful ones you would need later on in the development of whatever you were making.

And I hope for the day when Linux becomes another one of the many relics of computing which are no longer used.

The only thing the GPL protects against is good software ever being written.

Backwards compatibility is a relatively recent phenomenon in computing and even what we have today is far from perfect, with many programs from the 90's and mid 00's experiencing compatibility issues with modern OSs (or simply being broken such as with Mac programs that used endian-specific code when Apple switched from PPC to x86). But what end users and most programmers fail to see is the repercussions of demanding backwards compatibility.

What if I told you that CPUs could have an order of magnitude more compute for any given power consumption?
What if I told you that RAM could have an order of magnitude more throughput for any given number of PCB traces?
What if I told you that you could trust your operating system completely even though it might have some non-free/binary-blob components?
What if I told you that you could have an OS which was mathematically proven to be secure against attack?
Because we can do that now, but it would break backwards compatibility. It has forced a set of hardware and software paradigms upon computing and as a result has led us down a path of diminishing returns.

Many people only use Windows for things like Word, email, and internet. And to be honest I don't give a fuck about most computer users anyway.

Did you know that GNU has a system that does things like that? It's called GNU Hurd.