41–50 of 151 posts
Earlier quoted context omitted.
I wonder why all of these do not use gpl2?
Rust's technical choices seem to make releasing GPL software with it cumbersome and unattractive. Also the implied goal of a lot of Rust projects is to replace GPL'ed programs with permissive ones.
People really got to stop with crazy nonsense.
Earlier quoted context omitted.
I wouldn’t kneecap a OS project I wish to be adopted by licensing it GPL. Look at glibc which basically can’t practically support static linking. You make any of your OS standard libraries GPL and they need to suck to use and can’t statically link your code without being forced to also be licensed GPL. That viral property some people find desirable.
WRT kneecapping, history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of. Virality might suit the ego, but it doesn't make for a healthy project when its primary users are parasitic.
Software is not a scarce good. Let companies use free software without contributing back as much as they wish; it doesn't affect others in the least. There is no bleeding of the commons here, because even if companies take as much as they can without giving back, it doesn't reduce the resources available for others.
Earlier quoted context omitted.
Any government can get RCE on any OS with the change in their couch. Formal verification of process isolation is REALLY important when lives depend on it. That's a huge value add! My main concern is speed and the lack of capability based security. seL4 is faster than Linux by a mile and I'm guessing that this is much slower. You can put a POSIX layer on seL4 but POSIX is inherently flawed too. MAC separates privilege…
> Any government can get RCE on any OS with the change in their couch. Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation. If your statement was even remotely true then why is this not used in conflicts to devasta…
2) You haven’t seen a hot conflict yet
Earlier quoted context omitted.
WRT kneecapping, history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of. Virality might suit the ego, but it doesn't make for a healthy project when its primary users are parasitic.
> history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of. Software is not a scarce good. Let companies use free software without contributing back as much as they wish; it doesn't affect others in the least. There is no bleeding of the commons here, because even if companies take as much…
When that development gets silo'ed away in proprietary systems, that is potential development lost upstream. If that happens enough, upstream becomes starved and anemic, and with forks only living on in silos.
Apple, for example, has made trillions of dollars off of FreeBSD. To this day, FreeBSD still does not have a modern WiFi or Bluetooth stack.
Meanwhile, AMD, Intel, Microsoft, and even Apple, etc have full-time engineering roles and teams dedicated to upstreaming their improvements to Linux. And there are paid engineers at these companies that ensure WiFi and Bluetooth work on Linux.
Earlier quoted context omitted.
Any government can get RCE on any OS with the change in their couch. Formal verification of process isolation is REALLY important when lives depend on it. That's a huge value add! My main concern is speed and the lack of capability based security. seL4 is faster than Linux by a mile and I'm guessing that this is much slower. You can put a POSIX layer on seL4 but POSIX is inherently flawed too. MAC separates privilege…
> Any government can get RCE on any OS with the change in their couch. Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation. If your statement was even remotely true then why is this not used in conflicts to devasta…
The cost of internally developed exploits is probably much lower. They aren't one shot assets either, they can be used until someone plugs the hole.
There are private companies selling devices to law enforcement that can extract information from locked phones [2]. Availability of that sort of access to anyone's phone by local law enforcement is absurdly cheap.
[1]: https://opzero.ru/en/prices/
[2]: https://arstechnica.com/gadgets/2025/10/leaker-reveals-which...
OK can someone smarter than me educate me? A couple weeks ago I was curious what the strictest programming language was. ChatGPT listed a couple, and it kicked off a short discussion where I began asking it about the capabilities of stricter programming languages at low levels. Funny enough at the end it mentioned that SPARK/Ada was the strictest you could get at the lowest levels, same as Ironclad. At one point whil…
Lisps are perfectly usable for system level code as well. There was an entire lineage of Lisp Machines where virtually all OS code was written in lisp. Those probably could have used ACL2 had it existed.
There's an X-Y component to your questions though. The strictness of the programming language just isn't the main goal for OS formal verification. It just makes certain things easier. What's important is having executable semantics of the programming language, having a machine model, and a behavioral specification. All of these are typically written in proof languages, and the kernel code is proven to implement the behavior spec according to the machine and language semantics.
SPARK gives you executable semantics, but so do C (specifically the Clight subset), most of the Lisps, Rust, and many others. You're benefiting from certain errors being impossible in SPARK, but it's not a fundamentally different process.
Building new operating systems seems so ambitious to me. Radiant Computer ( https://radiant.computer/ ) was also recently posted. What other exciting projects like these exist?
https://asterinas.github.io/ (Linux compatible Kernel) and https://redox-os.org/ are two promising ones.
Building new operating systems seems so ambitious to me. Radiant Computer ( https://radiant.computer/ ) was also recently posted. What other exciting projects like these exist?
A guy can dream, at least.
Earlier quoted context omitted.
Any government can get RCE on any OS with the change in their couch. Formal verification of process isolation is REALLY important when lives depend on it. That's a huge value add! My main concern is speed and the lack of capability based security. seL4 is faster than Linux by a mile and I'm guessing that this is much slower. You can put a POSIX layer on seL4 but POSIX is inherently flawed too. MAC separates privilege…
> Any government can get RCE on any OS with the change in their couch. Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation. If your statement was even remotely true then why is this not used in conflicts to devasta…
since the 2010s atleast more than 140 countries spend over 10 mil a year on purly offensive cyber. most of those countries spend astronomical amounts more than that. that includes purchase of attack tools and exploits