I feel the same, because it seems that the only desktop-ready OS under GPL today is GNU/Linux, and it feels too bloated nowadays (not to mention that Linux is effectively stuck under GPLv2). Something like FreeBSD feels much lighter and better still being desktop‐ready. Looks like that guys from Hyperbola think the same and that’s why they are doing HyperbolaBSD. Btw there’s some progress in GNU Hurd, but they are still far from being desktop-ready.

There needs to be a new rule in technical discussion communities that outlaws bland comments that just spew "too bloated" and "feels much lighter". It is completely useless fluff description text.

No, it’s just you having some strange prejudices about these words (probably driven by blind faith in some overhyped technologies), so go better overregulate your preferred echo chamber.

No, it's from reading 20+ years of people who say this junk and it's demonstrably not backed up by the real world.

It's enthusiast tinker fantasy talk.

I had to laugh at the progress in gnu hurd. I've been hearing that one since the 90s

They now provide at least somehow working x86_64 images. It’s of course funny for a project started in the 90s to get x86_64 support only in the 2020s, but it’s still progress in relative terms.

IANAL, but you can’t actually just relicense code, even if it’s under BSD‐like license. What you can do is to release this code in the binary form without providing the source code.

Right you can add gpl code on top, but the base is still BSD

Correctness of the kernel and consistency of the theory implemented in it are different things. Gödel’s theorems prevent you from proving the latter, but not the former.

Interesting - what is correctness of the kernel here? That it faithfully implements the model?

Euclid’s Elements “rigorous proof” is not the same thing as the modern rigorous proof at all.

>But the infinitesimal methods used before epsilon-delta have been redeemed by the work on nonstandard analysis.

This doesn’t mean that these infinitesimal methods were used in a rigorous way.

“Paraconsistent logic” or “paraconsistent set theory” is what you are searching for.

I didn't think I'd get an answer to this, but awesome.