ratmice (u/ratmice) - Readit News

ratmice commented on CapROS: Capability-Based Reliable Operating System capros.org/... · Posted by u/gjvc

kragen · 18 hours ago

Hmm, do you know when?

ratmice · 17 hours ago

I wasn't able to google it, or find a public link to the email (but it was posted on a public list) so here is some relevant snippets from it.

Nov 20 2022 titled CapROS status

"When I retired a year ago I hoped to correct some of those issues, but I want to enjoy retirement and not just have a full-time unpaid job.", ...

"I am considering just abandoning CapROS. I believe there are some useful ideas in the system, but so far no one seems to have known or cared about them."

ratmice commented on CapROS: Capability-Based Reliable Operating System capros.org/... · Posted by u/gjvc

kragen · 18 hours ago

I mean, there isn't exactly a thriving ecosystem of existing software built for CapROS. Right now I don't think anybody even has CapROS itself building.

The problem has gotten a lot easier since the EROS days, thanks to Xen, QEMU, UEFI (?), and the explosion of cheap hardware, but it looks like maybe Charlie got sick or lost interest or something?

ratmice · 18 hours ago

Yeah, I did see a email on a capabilities list from him about him no longer working on it because of lack of feedback & wanting to just enjoy his retirement. That was the impression I got.

When he had resumed his work on it, I personally had been going through a back injury. I still feel bad that I didn't get a chance to contribute any of the hardware ports and software I wrote for it.

ratmice commented on CapROS: Capability-Based Reliable Operating System capros.org/... · Posted by u/gjvc

kragen · 18 hours ago

It's just you. seL4, CheriBSD, etc., do not fit your description. Neither did KeyKOS itself. You're presumably looking at research prototypes.

ratmice · 18 hours ago

I'd also note capros doesn't fit that description either. I don't know that there were examples that ran more than a single process.

That's probably not true, for anything relying on drivers since user mode drivers are basically processes there... but in the way that people might think of a process.

ratmice commented on 50 years of proof assistants lawrencecpaulson.github.i... · Posted by u/baruchel

ratmice · 3 days ago

I wish he had just said 50 years of LCF, since he even mentions automath in the article but that was but that was late 60s

ratmice commented on Nimony (Nim 3.0) Design Principles nim-lang.org/araq/nimony.... · Posted by u/andsoitis

xigoi · 10 days ago

Nim (the original one, not Nimony) compiles to C, so making basic types work differently from C would involve major performance costs.

ratmice · 10 days ago

Presumably unsigned want to return errors too?

Edit: I guess they could get rid of a few numbers... Anyhow it isn't a philosophy that is going to get me to consider nimony for anything.

ratmice commented on Nimony (Nim 3.0) Design Principles nim-lang.org/araq/nimony.... · Posted by u/andsoitis

xigoi · 10 days ago

If you need wraparound, you should not use signed integers anyway, as that leads to undefined behavior.

ratmice · 10 days ago

Presumably since this language isn't C they can define it however they want to, for instance in rust std::i32::MIN.wrapping_sub(1) is a perfectly valid number.

ratmice commented on Nimony (Nim 3.0) Design Principles nim-lang.org/araq/nimony.... · Posted by u/andsoitis

umanwizard · 10 days ago

What is the "even/odd theorem" ?

ratmice · 10 days ago

that all integers are either even or odd, and that for an even integer that integer + 1 and - 1 are odd and vice versa for odd numbers. That the negative numbers have an additional digit from the positive numbers ensures that low(integer) and high(integer) have different parity. So when you wrap around with overflow or underflow you continue to transition from an even to odd, or odd to even.

ratmice commented on Nimony (Nim 3.0) Design Principles nim-lang.org/araq/nimony.... · Posted by u/andsoitis

mwkaufma · 14 days ago

Big "college freshman" energy in this take:

  I personally prefer to make the error state part of the objects: Streams can be in an error state, floats can be NaN and integers should be low(int) if they are invalid (low(int) is a pointless value anyway as it has no positive equivalent).

It's fine to pick sentinel values for errors in context, but describing 0x80000000 as "pointless" in general with such a weak justification doesn't inspire confidence.

ratmice · 10 days ago

Without the low int the even/odd theorem falls apart for wrap around I've definitely seen algorithms that rely upon that.

I would agree, whether error values are in or out of band is pretty context dependent such as whether you answered a homework question wrong, or your dog ate it. One is not a condition that can be graded.

ratmice commented on Shai-Hulud Returns: Over 300 NPM Packages Infected helixguard.ai/blog/malici... · Posted by u/mrdosija

sph · 21 days ago

It's not "node" or "Javascript" the problem, it's this convenient packaging model.

This is gonna ruffle some feathers, but it's only a matter of time until it'll happen on the Rust ecosystem which loves to depend on a billion subpackages, and it won't be fault of the language itself.

The more I think about it, the more I believe that C, C++ or Odin's decision not to have a convenient package manager that fosters a cambrian explosion of dependencies to be a very good idea security-wise. Ambivalent about Go: they have a semblance of packaging system, but nothing so reckless like allowing third-party tarballs uploaded in the cloud to effectively run code on the dev's machine.

ratmice · 21 days ago

My feeling is that languages with other packing models are merely less convenient, and there is no actual tangible difference security-wise. Just take C and replace "look for writable repositories". It just takes more work and is less uniform to say write a worm that looks for writable cmake/autoconf and replicate that way.

What would actually stop this is writing compilers and build systems in a way that isolates builds from one another. It's kind of stupid that all a compiler really needs is an input file, a list of dependencies, and an output file. Yet they all make it easy to root around, replicate and exfiltrate. It can be both convenient and not suffer from these style of attacks.

ratmice commented on GCC SC approves inclusion of Algol 68 Front End gcc.gnu.org/pipermail/gcc... · Posted by u/edelsohn

wahern · 23 days ago

Until a few years ago, gccgo was well maintained and trailed the main Go compiler by 1 or 2 releases, depending on how the release schedules aligned. Having a second compiler was considered an important feature. Currently, the latest supported Go version is 1.18, but without Generics support. I don't know if it's a coincidence, but porting Generics to gccgo may have been a hurdle that broke the cadence.

ratmice · 23 days ago

Seems doubtful, given that generics and the gccgo compiler were both spearheaded by Ian Lance Taylor, it seems more likely to me that him leaving google would be a more likely suspect, but I don't track go.