mimd

I was never great at spelling. But at least it now has the plus of showing I'm not AI.

I'm not fully sure of what is the total composition of opinions, and will not dismiss your experience. Indeed the hyper privacy all high costs group might be a small percentage. But I know several that use tails openly, despite being vehemently protective of women, while knowing less men that use tails. Certainly not "mythical" in my book. Futhermore the ignoring of viewpoints of non-tech women, the majority of women, expressing constant worry of state discrimination via information collection even though it's regularly hitting the news is bad. Tech is not the only party to this, indeed that's one of the reasons for this scenario as he correctly pointed out. His claim was overbroad so as to improve his argument, an annoying manipulation. Additionally, he used emphasis on wife/daughter, yet not including their voices, while minimizing his own position, which warrants the further parthian shot.

I have met women in tech who have been privacy conscious and paranoid about state control. Or even a healthy stream of non-tech women worried that it will be used to attack their sex and to discriminate. I don't think the author is correct in his belief that there are not a considerable amount of women worried about privacy. And to make such a board claim, and in light of my experience, would indicate either hubris or sexism.

If anything, he frames that he is concerned about his daughter as a father. The viewpoint of patriarchy.

So, no one's buying our textbooks anymore, it's getting costly to do our work, stop over claiming results for your marketing and insulting our work? I would have stuck with that.

Everything else seems to be organizational or standard politics. I would have avoided the political sections as it just sets those signatories up for getting into those fights, having not realized what they cosigned.

The issue of attribution is a hard problem that has festered for a while, that has mostly been obscured by the inability to discern an authors entire body of ingested information. I would be careful as, the proposed opt-out restrictions will be eventually imposed on people, which sorta blows up the whole math enterprise of universities/etc. Ie. the proposed leads to a book author revoking a person's ability to reference their arguments in a mathematic paper for money, spite, etc.

New to the field? Intel did xeon max in the last gen, with 64GB HBM 2e, 1.6TB/s per 56 cores. It was not a great success.

The nice thing about the Internet is that a person, great or small, can voice their grandiose and yet myopic views of a problem and their absurd solutions to it...freely.

Considering that the rant is using photos from Star Trek and Oliver Twist to make their points, copyrighted material with no indication of permission, they're less "creative" than a stochastic parrot.

I'm annoyed at the cost statement, as that's the sleight of hand. "$20000" at current pricing. Add some orders of magnitude to the costs and you'll get your true price you'll have to pay when the VC money starts to wear off. 2nd, this is ignoring the dev time that he/others put in over multiple iterations of this project (opus 4, opus 4.5) and all the other work to create the scaffolding for it, and all the millions/tens of millions of dollars of hand written test suits (linux kernel, gcc, doom, sqlite, etc) he got to use to guide the process. So add some more cost on top of that orders of magnitude increase and the dev time is probably a couple months/years more than "2 weeks".

And this is just working off the puff pieces statements, and not even diving into the code to see it's limits/origins, etc. I also don't see the scaffold in the repo, as that's where the effort is.

But still it's not surprising, from my own experience, given a rigorously definable problem, enough effort, grunt work, and massaging, you can get stuff out of the current models.

Opensource is a bit more complex than being a "public good". They're focusing on the low cost as a jump starting point, which make me doubt their sincerity/understanding about managing that relationship healthily.

It's not going to solve the housing issue and is mostly for press (and it's not even getting into ulterior motives), but it might help with preventing a longer term issue of large investors becoming a major issue. Additionally, I wonder about the choice in properties as properties aren't fungible.

Huzzah! You made it to the big leagues Rust! Come join C over here with the "CookiesVE".

I suggest waiting till the gcc side matures, with the minimum of a working gcc frontend for a non optional dependency. Optional dependencies with gcc_codegen might be okay. Git is pretty core to a lot of projects, and this change is risky, it's on a fairly short time frame to make it a core dep (6 months?).

Rudimentary analysis of five battles spread out over a 1500 year period; supposedly supporting sources that upon examination state their unsureness; stating propaganda casualty numbers without a hint of irony to justify; allows you to unequivocally state that no one did volly fire? Ugh.

No, it can track pointer bounds and validity across functions. It also targets identifying cases of UB via eva. Both rust and frama-C rely on assertions to low level memory functions. Rust has the same gaping UB hole in unsafe that can cross into safe.

If we are talking about more than memory, such as what greg is talking about in encoding operational properties then no, rust is far behind both frama-C, Spark, and tons of others. They can prove functional correctness. Or do you think miri, kani, cruesot, and the rest of the FM tools for Rust are superfluous?

My mocking was that that the kernel devs have had options for years and have ignored them out of dislike (ada and spark) or lack of effort (frama-C). That other options provide better solutions to some of their intrests. And that this is more a project exercise in getting new kernel blood than technical merits.

Yes, I know the policy that has been stated and the recent docs on it (https://rust-for-linux.com/rust-kernel-policy). A good portion of the R4L group were trying to avoid this scenario due the toxicity of such a change (especially at this early contentious point, and despite what their online advocates want). I don't think the policy will immediatly change because of his statements, but I find it pretty clear that this is where he wants the project to go.

"But for new code / drivers..." encompasses more than just "drivers" and refers to all new code. I doubt it's a mistake either due to the way the rest of the email is written. And Greg said "no one sane ever thought that (force anyone to learn rust)" just 5 months ago (https://lkml.org/lkml/2024/8/29/312). But he is now telling his C devs they will need to learn and code rust to make new code in the kernel.

https://llvm.org/devmtg/2023-05/slides/TechnicalTalks-May11/...

Supposedly ~5% (1-29%), but I'm testing my own projects to verify (my guess is higher at 10-20%, but will depend on the code). Supposedly it's to land in gcc at some point but I dunno the time table.

Yes, panicking in kernels is bad. I've followed the whole R4L fight about working around it.

https://github.com/apple-oss-distributions/xnu/blob/main/doc...

https://github.com/apple-oss-distributions/xnu/blob/main/doc...

Upstream fbounds in xnu has options for controlling if it panics or is just a telemetry event. They are in a kernel situation and have the exact same considerations on trying to keep the kernel alive.

Isn't this a bait and switch, that all the c kernel devs were complaining about? That it wouldn't be just drivers but also all new kernel code? The lack of candor over the goal of R4L and downplaying of other potential solutions should give any maintainer (including potential rust ones) pause.

Anyway, why just stop at rust? If we really care about safety, lets drop the act and go make everyone do formal methods. Frama-C is at least C, has a richer contract language, has heavy static analysis tools before having to go to proofs, is much more proven, and the list goes on. Or, why not add Spark to the codebase if we are okay with mixing langs in the codebase? Its very safe.

If you look at the CVE lists, about 70-80% of all c memory bugs are related to OOB Read and Write. Additionally, like rust, fbounds-safety can remove redundant checks if it can determine the bounds. My question is how likely can it be adopted in the kernel (likely high).

I will need to read their conversations more to see if it's the underlying fear, but formalization makes refactoring hard and code brittle (ie. having to start from scratch on a formal proof after substantially changing a subsystem). One of the key benefits of C/Kernel have been their malleability to new hardware and requirements.

Well, it will be really funny when the executive branch starts firing all the judiciaries security (USMS JSD, under DoJ) to save costs. But secondary outcomes have either not dawned or dissuaded the recent courts on their path to increasing executive power.

Of course they are. Any rational person not blinded by partisanship would be infuriated by this development and immediately demand that DOGE be restrained. Even most partisans would blanch and demand accountability. DOGE advocates know this. Their only recourse is to try to hide it or distract everyone with tangential arguments like they are doing in this thread.

https://www.npr.org/2025/02/14/nx-s1-5298190/nuclear-agency-...

If even half of NPR's report is true, the way in which it was conducted was grossly cruel and with complete ignorance.

DOGE and it's supporters are quiet literally playing like a child with the levers that decide if you wake up tomorrow.

Since the rest of the advisory is demanding full scale rewrites into a new language based on llvm that has officially nuetered it's gcc port, I don't think they really care about those sorts of concerns. Hence my annoyance at their proposal. The fbounds devs do, as the design allows for modified source to be still compilable in alternative toolchains that do not support fbounds (you can remove them via macros) and they are working to add it to gcc. And I don't think its going to matter much soon if it's limited to gcc/llvm, as all the proprietary vendors left and right are dropping their 30+ year compilers to piggyback off llvm (I don't exactly agree with this btw, but it is what it is).

Not to fully encapture C's variadic printf, but on the macro front, I've been having fun creating type checking for macros by a constexpr allocation from a _generic switch type check of the args and then checking the result with static_asserts. I think there was a hack before as you mentioned but would have to dig through my tests to find it, but the C23 version is quite clean. Might want see if I can get it to be clean for a variadic printf version.

I wish they would have gone more indepth about the current compiler work, such as stack defenses or fbounds-safety. It should cover OOB read and write safety, which is 70-80% of C's memory vulnerabilities, for a marginal performance overhead and with abi compatibility.

https://clang.llvm.org/docs/BoundsSafety.html

I know this article is more a buisness case presentation than a full demonstration of the field but the TR also misses some points.

Why remove the refrences in the TR to frama-C, cbmc, etc. from the opinion report? They are easier to adopt than the heavier tooling of coq, etc. I'm always suprised to see those tools ignored or downplayed, when it comes to these discussions. I do agree with the TR's sentiment that we need to improve accessibility and understanding of these tools, but this is not a great showing for that sentiment.

Additionally, both articles miss that compiler modified languages/builds are a path, such as fbounds-safety. They will be part of the solution, and frankly, likely the biggest part at the rate we are going. Eg. current stack defenses for C/C++/Rust, unaddressed in safe language design, are compiler based. The compiler extension path is not particularly different than cheri, which requires a recompile with some modifications, and the goal of both approaches is to allow maintainers to band aid dependencies with minimal effort.

The TR handwaves away the question of the complexity of the development of formal method tools for Rust/Unsafe Rust and C++. Ie. rust really only has two tools at the moment: miri and kani (which is a cbmc wrapper). Heavier tools are in various states of atrophying/development. And C++ support from the c family of formal tools such as frama-C, is mostly experimental. It's not assured, that with the continued language development rate of both languages and the complexity of the analysis, that the tools for these languages will come forth to cover this gap anytime soon.

I do not think the claim in the TR that the current unsafe/safe seperation will result in only requiring formal analysis of the unsafe sections is true, as logical errors, which are normal in safe rust, can cross the boundries to unsafe and cause errors, thus nessecitating whole program analysis to resolve if an unsafe section could result in errors. Perhaps it will decrease the constants, but not the complexity. If rust does further restricts perhaps more of the space could be covered to help create that senario, but the costs might be high in both usability and so on.

Thanks for the input and links. I'll need to test out the costs of the mitigations.

BTW, I found one of the rust rfc documents helpful for understanding the borrow checker. Do you know if there is a similar rust RFC document for the upcoming polonius borrowchecker, even if it's just a working copy? I'm having trouble finding anything beyond some blog posts.

If it requires the programmer to bear the responsibility for proper usage (eg. must use checked_add not rely on panic), how's that different than the issues with undefined behavior? I'm also concerned with the differing functional behavior between debug and release, and the mistaken impression it could create (eg. code handles overflow in debug fine due to panic but blows up on release as the proper solution is not used). And a resulting propagation of the overflow error to a precondition of an unsafe call that modifies memory.

I'm confused over lines such as "Profiles have to reject pointer arithmetic, because there’s no static analysis protection against indexing past the end of the allocation." Can't frama-c/etc do that? Additionally, section 2.3 is narrower than what is implied by the words "safe" and "out-of-contract" and is more concerned with what C/C++ call "undefined behavior" requirements than contract correctness. Ie. An integer which is defined to wrap overflows and violates the requirement of the function contract, which I can cause in a safe release build rust.