I want to preface this with "This isn't a gotcha".
I think you make an important oversight with these claims, which is that you can enforce logical safety over a memory unsafe language and have a much higher degree of safety than memory safety. Formally verified C doesn't change the language, you can in principle take C code run through compcert and compile it elsewhere. It's still a memory unsafe language, but we can express a much higher degree of safety than simple memory safety.
Another aspect to consider is that all garbage collected languages are memory safe. A language like Python actually has a far greater degree of memory safety than a language like Rust because it offers no ability to break memory safety (without calling into foreign code), while Rust lets you do it within unsafe blocks using raw pointers. That being said, anybody who would suggest using Python over Rust in a security-focused context is completely out of their mind.
In serious places where security is critical and margin for error is low, formal verification has existed for decades and is the standard. Any operation - specifically in the context where security is critical - which is not formally verifying its software is a mickey mouse operation, because they're fundamentally compromising on security to an unacceptable degree. I think it would be nice to have a formal verification toolchain and language extension for Rust to allow for full logical safety, but last I checked this area was still a work in progress for the language.
I know anytime Rust is brought up, someone brings up logical safety, and patterns are annoying. Rust obviously has a lot of tricks up its sleeve to automatically detect issues that a language like C++ cannot. Naive Rust is preferable over naive usage of a memory unsafe language. The problem is that in a serious security critical context, "naive" is completely unacceptable. If security is a core goal, there can be no replacement for fully blown logical safety enforcing strict behavioral and structural guarantees in every single facet of the codebase. I know the line, that logical safety is excruciatingly labor intensive and so the tradeoff with using Rust is that it affords some of the safety of formally spec'd and proven code. The problem is that the amount it affords you is completely marginal. The safety gap between C and Rust is much smaller than the safety gap between Rust and formally proven correct SPARK. It's just the reality. I'm loathe to see a future where marketing hype sees a degeneration of tools because it was presented as a serious alternative.
It's just provencial nonsense, there's no sound reasoning to it. Reductionism being taken and used as a form of refutation is a pretty common cargo culting behavior I've found.
Overwhelmingly, I just don't think the majority of human beings have the mental toolset to work with ambiguous philosophical contexts. They'll still try though, and what you get out of that is a 4th order baudrillardian simulation of reason.
"Just" is used here as a reductive device. You reduce others to a few sentences.
Sentences constructed of words and representations of ideas defined long before you existed. I question whether you can work with ambiguous contexts as you have had the privilege of them being laid out in language for you already by the time you were born.
From my reference frame you appear to merely be circumlocuting from memory, and become the argument you make about others.
> Your HTTP client, cli utility helper, whatever library is not a consumer product.
I'm not sure how the author came to this conclusion.
At any rate, programmers aren't any worse about this than mathematicians. Just replace [fictional name] with some foreign word or philosophical term that's justified with the most insane mental gymnastics you've ever heard of. Given some historical native speaker of Latin, do you think they're going to know what a matrix is for? No, because the word means "uterus". There is no connection to "tabular shorthand of linear transformations."
I think it's clear the author is writing this to vent frustration, but I think they've misidentified the actual problem:
> http-request-validator is infinitely superior to “zephyr” when someone is scanning dependencies at 2 AM debugging a production incident.
My jaw hit the floor reading this. The idea there are people out there debugging codebases without knowing something as foundational as the dependencies is beyond absurd to me. That's insane and horrifying, overshadowing pretty much the entire blog post. Does anyone else live like this? How do you tolerate these conditions? Why would you tolerate these conditions?
Can these claims back themselves up with a study showing that over a large population size with sufficient variety, sourced from a collection of diverse environments, LLM output across a period of time is more reliably correct and without issue when outputting Rust? Otherwise this is nothing but unempirical conjecture.
Ah the classic "show me ironclad evidence of this impossible-to-prove-but-quite-clear thing or else you must be wrong!"
Although we did recently get pretty good evidence of those claims for humans and it would be very surprising if the situation were completely reversed for LLMs (i.e. humans write Rust more reliably but LLMs write C more reliably).
Actually it's the classic "inductive reasoning has to meet a set of strict criteria to be sound." Criteria which this does not meet. Extrapolation from a sample size of one? In a context without any LLM involvement? That's not sound, the conclusion does not follow. The point being, why bother making a statistical generalization? Rust's safety is formally known, deduction over concrete postulates was appropriate.
> it would be very surprising if the situation were completely reversed for LLMs
Lifetimes must be well-defined in safe Rust, which requires a deep degree of formal reasoning. The kind of complex problem analysis where it is known that LLMs produce worse results in than humans. Specifically in the context of security vulnerabilities, LLMs produce marginally less but significantly more severe issues in memory safe languages[1]. Still though, we might say LLMs will produce safer code with safe Rust, on the basis that 100,000 vibe coded lines will probably never compile.
I never claimed to be doing a formal proof. If someone said "traffic was bad this morning" would you say "have you done a scientific study on the average journey times across the year and for different locations to know that it was actually bad"?
> LLMs produce worse results in than humans
We aren't talking about whether LLMs are better than humans.
Also we're obviously talking about Rust code that compiles. Code that doesn't compile is 100% secure!
I didn't claim that you were doing formal proofs. You can still make bad rhetoric, formal or not. You can say "The sky is blue, therefore C is a memory safe language" and that's trivially inferred to be faulty reasoning. For many people bad deduction is easier to pick up on than bad induction, but they're both rhetorically catastrophic. You are making a similarly unsound conclusion to the ridiculous example above, its not a valid statistical generalization. Formal or not the rhetoric is faulty.
> would you say "have you done a scientific study on the average journey times across the year and for different locations to know that it was actually bad"?
In response to a similarly suspiciously faulty inductive claim? Yeah, absolutely.
> We aren't talking about whether LLMs are better than humans.
The point I'm making here is specifically in response to the idea that it would "be surprising" if LLMs produced substantially worse code in Rust than they did in C. The paper I posted is merely a touch point to demonstrate substantial deviation in results in an adjacent context. Rust has lower surface area to make certain classes of vulns under certain conditions, but that's not isomorphic with the kind of behavior LLMs exhibit. We don't have:
- Guarantees LLMs will restrict themselves to operating in safe Rust
- Guarantees these specific vulnerabilities are statistically significant in comparative LLM output
- The vulnerability severity will be lower in Rust
Where I think you might be misunderstanding me is that this isn't a statement of empirical epistemological negativism. I'm underlining that this context is way too complex to be attempting prediction. I think it should be studied, and I hope that it's the case LLMs can write good, high quality safe Rust reliably. But specifically advocating for it on gut assumptions? No. We are advocating for safety here.
Because of how chaotic this context is, we can't reasonably assume anything here without explicit data to back it up. It's no better than trying to predict the weather based on your gut. Hence, why I asked for specific data to back the claim up. Even safe Rust isn't safe from security vulnerabilities stemming from architectural inadequacies and panics. It very well may be the case that in reasonably comparable contexts, LLMs produce security vulnerabilities in real Rust codebases at the same rate they create similar vulnerabilities in C. It might also be the case that they produce low severity issues in C at a similar statistical rate as high severity issues in Rust. For instance, buffer overflows manifesting in 30% of sample C codebase resulting in unexploitable segfaults, vs architectural deficiencies in a safe Rust codebase, manifesting in 30% of cases, that allow exfiltration of everything in your databases without RCE. Under these conditions, I don't think it's reasonable to say Rust is a better choice.
Again, it's not a critique in some epistemological negativist sense. It's a critique that you are underestimating how chaotic this context actually is, and the knock-on effects of that. Nothing should surprise you.
I've found usually to poor effect. Both Rust and Haskell did away with .mli files and ended up worse for it. Haskell simplified the boundary between modules and offloaded the abstractions it was used for into its more robust type system, but it ended up lobotomizing the modularity paradigm that ML did so well.
Rust did the exact opposite and spread the interface language across keywords in source files, making it simultaneously more complicated and ultimately less powerful since it ends up lacking a cognate to higher order modules. Now the interfaces are machine generated, but the modularity paradigm ends up lobotomized all the same, and my code is littered with pub impls (pimples, as I like to call it) as though it's Java or C# or some other ugly mudball.
For Haskell, the type system at least copes for the bad module system outside of compile times. For Rust, it's hard for me to say anything positive about its approach to interfaces and modules. I'd rather just have .mlis instead of either.
That qualifier only makes the anthropormorphization more sound. Have you actually thought it through? Give an untrained and unspecialized human the power to cause significant loss of life in a medical context in the same exact capacity, and it's all but guaranteed that's the outcome you'll end up with.
I think it's important to be skeptical and push back against a lot of the ridiculous mass-adoption of LLMs, but not if you can't actually make a well-reasoned point. I don't think you realize the damage you do when the people gunning for mass proliferation of LLMs in places they don't belong can only find examples of incoherent critique.
An untrained and unspecialised human can be trained quickly and reliably for the cost of meals and lodging and will very likely actually try to do the right thing because of personal accountability.
Delegating responsibility to badly-designed or outright unfit-for-purpose systems because of incoherent confidence is plainly a bad plan.
As for the other nuances of your post, I will assume the best intention.
one of the weirdest and most off-putting parts of macos for me was that dyld isn't aware of that standardized location. a lot of curious oversights the more you pick at it.
What do you mean? I can just tell the linker to link against something in the shared cache and it finds it. It’s been as simple as `-framework <FrameworkName>`
I’ve never had to do extra work to find a system vendored dylib in my decades of supporting cross platform apps.
They probably mean that they don’t like the way the “install name” (as it’s referred to) of a shared library is embedded in the library and then copied to whatever links the library, and is then used to find the library at runtime. I suspect they’d prefer to build the shared library with an arbitrary install name and then just have it found automatically by being in the Frameworks or Libraries directory.
Most platforms don’t have a concept of “install name” distinct from the library name; the value was originally the full path to the deployment location of the library, which was revised to support meta-paths (like `@rpath/LibraryName`) in Mac OS X 10.4 and 10.5 and is what the runtime dynamic loader (dyld) uses to match a library at load time. So an application’s executable can have a set of self-relative run path search paths, which is how it can load libraries from its Frameworks and Libraries directories.
Depends on whether you’re building with Xcode; when I worked on it, I ensured that the templates included with Xcode would have the right setup to declare appropriate run path search paths for applications, and appropriate install names for frameworks and (shared) libraries.
However when building with just command line tools and not passing all the same arguments an Xcode project and target causes to be passed, you have to do extra work to ensure the right run path search paths get into built executables and the right install names get into built libraries and frameworks.
That latter is to ensure that if you don’t pass those extra arguments, executables and shared libraries are built for Darwin-based platforms as much as reasonably possible like they are on other UNIX-like platforms.
I mean I had to manually patch the rpaths of macos binaries distributed as an app bundle, because dyld didn't have the relative location of the shared libs in the app bundle in its search path. Not a huge deal, since patching rpaths was also part of the other Unix pipelines, the reasoning was just different. Patching rpaths on other platforms was because we were distributing dependencies in the base directory of the application, which isn't the standard way to do things. On mac, it was because the dynamic linker wasn't aware of app bundle structure for some reason, which is a weird disconnect between an OS standard and a basic system component.
I think you make an important oversight with these claims, which is that you can enforce logical safety over a memory unsafe language and have a much higher degree of safety than memory safety. Formally verified C doesn't change the language, you can in principle take C code run through compcert and compile it elsewhere. It's still a memory unsafe language, but we can express a much higher degree of safety than simple memory safety.
Another aspect to consider is that all garbage collected languages are memory safe. A language like Python actually has a far greater degree of memory safety than a language like Rust because it offers no ability to break memory safety (without calling into foreign code), while Rust lets you do it within unsafe blocks using raw pointers. That being said, anybody who would suggest using Python over Rust in a security-focused context is completely out of their mind.
In serious places where security is critical and margin for error is low, formal verification has existed for decades and is the standard. Any operation - specifically in the context where security is critical - which is not formally verifying its software is a mickey mouse operation, because they're fundamentally compromising on security to an unacceptable degree. I think it would be nice to have a formal verification toolchain and language extension for Rust to allow for full logical safety, but last I checked this area was still a work in progress for the language.
I know anytime Rust is brought up, someone brings up logical safety, and patterns are annoying. Rust obviously has a lot of tricks up its sleeve to automatically detect issues that a language like C++ cannot. Naive Rust is preferable over naive usage of a memory unsafe language. The problem is that in a serious security critical context, "naive" is completely unacceptable. If security is a core goal, there can be no replacement for fully blown logical safety enforcing strict behavioral and structural guarantees in every single facet of the codebase. I know the line, that logical safety is excruciatingly labor intensive and so the tradeoff with using Rust is that it affords some of the safety of formally spec'd and proven code. The problem is that the amount it affords you is completely marginal. The safety gap between C and Rust is much smaller than the safety gap between Rust and formally proven correct SPARK. It's just the reality. I'm loathe to see a future where marketing hype sees a degeneration of tools because it was presented as a serious alternative.
reply