Because the desperation to have kids in the US from the religious outweighs the need to use it as an end around to attack lgbtq/disabled people so far.
147 karma · joined September 2, 2020
If anything, he frames that he is concerned about his daughter as a father. The viewpoint of patriarchy.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.