grumblenum

>I'm interested in seeing the problems solved, and I'm indifferent to technology.

I think the first problem is some kind of language specification. That it's not possible to know what behavior one should expect from rustc means that it isn't a solution. It's another problem. You should check out Ken Thompson's great speech on why this is an issue. https://www.cs.cmu.edu/~rdriley/487/papers/Thompson_1984_Ref...

Or do you think it's wrong to regard unauditable enhancements to free software paid for by Google with suspicion?

Zircon is a kernel.

My point is that solicitations for grant money do not provide the assurance that products that actually exist do.

So dead "because I said so" in essence?

I don't think that the mere existence of a "working group" or grant funded research positions for verifying rustc or a subset thereof is the same as having a verified compiler. That's certainly not a strong argument to against using rustc for safety over one of the many verified compilers that actually exist. At least, I didn't see in the "rustbelt" list of papers anything which appeared to indicate that a verified compiler or language subset do in fact exist. Furthermore, that the proposed patches rely on the nightly compiler and a special variant of rust's core, which can only be enforced by special feature tags seems to suggest that Rust-Linux is not being written in this hypothetical, future compiler.

>the fact is that Rust has a larger and growing mindshare so this effort is unsurprising.

I think that is a false perception created by the dev-blogging community. Based on GitHub activity (https://madnight.github.io/githut/#/pull_requests/2021/2) Rust usage is declining (absolute numbers show little growth). Based on developer surveys (https://www.jetbrains.com/lp/devecosystem-2020/) very few people use rust outside of hobby development.

I think the concern is that the core argument that "I think Linux should adopt rust for safety" is a bit dishonest, given that there are a large number of well-vetted alternatives. "I think Linux should adopt rust because I like rust for social reasons" would probably be more correct. That Google staff seem to think rust is good for the Linux kernel but not, say, Zircon, would be surprising if those same people actually believed that any legal rust program is safe and inherently trustworthy. "Embrace, extend, extinguish" wasn't that long ago.

As one of the developers of this patchset, can you comment on how these contributions will be licensed? Can you also comment on how a third party can verify or audit the output of a compiler without a specification?

>just that it's empirically likely to solve the problem.

Can you comment on what empirical evidence you based this statement on?

Why are you using past tense for Ada? Adacore is still doing business and Ada 202x will be standardized this year or next.

I’m also not sure why “nice JSON libraries” is a hard requirement for kernel code. Also, see JWX.

Types that can be defined by users are, necessarily, part of a language syntax, so that they are aligned with the syntax is just a tautology. Equating user defined types with formal verification is just nonsense. C has types. Python has types. Rust has types. That the program does what you think it should do does not logically follow the mere existence of types. I have no idea what "in the large" is supposed to mean. I feel like GPT-3 is arguing with me.

> focusing purely on type- and memory-safety, not conformance to arbitrary specifications

What are types if not arbitrary specifications? Are you suggesting that formally verified software is not memory safe? What on earth does "scalable" even mean? A verified program cannot scale? If not, why not?

I was under the impression that SeL4 exists.

So why not formal verification or static analysis tools of an existing codebase (Frama-C)? Or dropping in C derived from a formally verified source (Idris / F-Star)? Or a language with good performance and a verified subset (Ada/Spark)?

I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates.

>I'd rather see a new kernel optimised and written in Rust from scratch rather than dragging the legacy skeletons around and also bringing the vulnerabilities with us.

There is Redox, which was intended to be practical, but I'm not aware of much public interest in that. Phillip Oppenheimer blogged about one too, I think, but that's explicitly academic.

I'm hoping that somebody will maintain a Linux fork called "stainless." Really, the jokes write themselves.

On a more serious note, I am curious to see what license RIIR Linux will have.

Diffusion of responsibility and the tragedy of the commons are pretty textbook psychological phenomena that I’m surprised more people seem to be unaware of. I would be surprised if any committee with custody of any asset were prepared to take quick, decisive, and costly action in the long-term interest of said asset.

CT > 40 then vs CT 28 now. I can't help but be reminded of "yellowcake."

I can see how hardware handling of switching, some filtering and maybe stripping TLS is feasible. Since you're knowledgeable of the subject, how would you index that information for future retrieval, which could be anything in the set of all digital representations of information in all possible languages and encodings? How would you determine what information is important?

No, Snowden is portrayed as a hero. Emmanual Goldstein is "whiteness".

No, but I think it's unlikely that anybody, including the NSA, can collect, index, catalog and parse meaning out of hundreds of GB _per second_ (I'm using Statista numbers for global IP traffic). I would be skeptical that it's even physically possible with any amount of hardware in existence. If you really want a concentrated haul of the most interesting stuff, then I would say that platforms which openly market themselves as safe venues for criminals and dissidents would be strong candidates. You would still have extraordinary data warehousing needs just for that limited subset of traffic.

Where I live the market rate was $100-125/sqft for single-family before the lumber supply squeeze. I think you just happen to live somewhere where inflation effects are ahead of the rest of us.

Is there a clear definition of what ZTA even is? I read the O'Reilly book, and as best I can tell, the advice was fairly obvious recommendations and also 'replace your firewall as a single point of failure and make your access-control system your single point of failure'.

My pet theory is that Snowden's disclosure is both a bit of CIA/NSA sibling rivalry and a misinformation campaign to scare people into thinking that the NSA has far more surveillance capabilities than it really does. The goals being to frighten people into inaction and to herd them onto platforms these entities can monitor (TOR & ANOM come to mind).

That Snowden is able to rake in book and movie deals while 'on the run' makes me doubt that anybody is actually interested in catching him.

So someone who isn't you should pay for its development cost, manufacture, quality control, shipping, storage, and distribution? Or should the people who do those things be conscripted into labor for the glory of these heartfelt convictions?

Prior to 100 years ago, this conditions would have just been fatal. That you can keep yourself alive today for less than the cost of your mobile phone bill is a pretty good value proposition. I just don't understand the outrage.

And what would you say that those goals are?

If he’s doing the CE&I and let it pass, then he has nobody to blame but himself. Knowing it’s wrong and certifying that it’s right entails a lot of professional risk in this industry. I suspect his concerns aren’t too serious or someone else is certifying the work.

One other situation I can imagine is that the risk is outside his domain. Example: I saw a company scrape flat clays out of a roadway and use that material as fill for slab-on-grade foundations of duplexes. I wouldn’t expect those to last long, but the developer is also the owner, so he’s only hurt himself. I don’t find the owner to be particularly sympathetic, I only certified the road construction, and the only person to report the poor practice to is the owner himself, who also hired the crew.

Yeah, a Code Enforcement department for a large municipality would pay for reporting automation. I don’t think it would prevent this event. It’s a condo, so the building is probably maintained by a POA. Who would have an incentive to inspect the building? Who has a contractual obligation for maintenance? POA members. Who has to pay for repairs? POA members. Who now has an incentive to avoid repairs? POA members. Would you dime yourself out to be on the hook for repairs that may exhaust your discretionary income for many, many years? Or would you “touch up the X-ray” as Warren Buffet put it?

POAs are a terrible idea and I wish they didn’t exist. Distributed ownership always seems to incentivize bad behavior.

Poor soils can be managed with good foundations. You can put a building on water with the right foundation design. In the case of an office, the safety factors in design are usually pretty high. I’m assuming soil sampling is for modified proctor density. Usually, the criteria for those are fairly arbitrary. Some soils are so sensitive to moisture content that density measurements aren’t very informative. Not blowing up a multi-million dollar construction schedule over a few mm of consolidation is probably a reasonable take.

I think market incentives to do the right thing is more helpful than an app.

Mark Zuckerberg made some substantial (100s of millions I’ve read) donations to the DNC and proxies. It would be surprising that they would then almost immediately try to destroy his company. A quid pro quo is pretty believable.

Moderation is also why you won’t see comments which are impolite or heretical but may be obviously true. 4chan is moderated, but the goals are just very different from sites that want to avoid the hassle of vigilante activists by enforcing orthodoxy in content. 4chan also goes to some effort to ensure easy identification of its pseudo-anonymous users. It’s also useful fodder to trick people into rage-donating to the right party. Always ask what the business model is for popular web properties. If you can’t figure it out or nobody else can make money in the same domain, then there is probably a side channel being monetized.