Absolutely. See DeepSeek Prove, for instance. As far as I understand, it's basically a neurosymbolic system, which uses an LLM to write down proofs/code, then Lean to verify them, looping until it finds a proof/implementation that matches the specification, or it gives up.
> I think the chance that your Rust application is going to be more performant or efficient than C, is whether you are focused on writing performant and efficient code.
I believe that depends on the sophistication of algorithms. High-level algorithms (especially if they involve concurrency or parallelism) are much easier to write in Rust (or in C++) than in C, which gives them a pretty good chance to be at least as fast as any reasonably safe C implementation.
For low-level algorithms, of course, it's really hard to beat polished C code.
> Out-of-the-box, I’m guessing people will use too many cargo packages, each that are over-engineered or written by less-experienced developers, so it will be less efficient and less performant.
I don't think that this is going to be a problem. The Tor Project developers I've interacted with sounded quite serious about security. Forbidding non-blessed cargo packages is pretty trivial.
> In addition, you could more easily inadvertently introduce security problems.
> Maybe our future is like the one depicted in Severance - we look at computer screens with wiggly numbers and whatever “feels right” is the right thing to do. We can harvest these effortless low latency “feelings” that nature gives us to make AI do more powerful work.
Come to think about it... aren't this exactly what syntax coloring and proper indentation are all about? The ability to quickly pattern-spot errors, or at least smells, based on nothing but aesthetics?
I'm sure that there is more research to be done in this direction.
I suspect that we're going to witness a (further) fork within developers. Let's call them the PM-style developers on one side and the system-style developers on the other.
The PM-style developers will be using popular loosely/dynamically-typed languages because they're easy to generate and they'll give you prototypes quickly.
The system-style developers will be using stricter languages and type systems and/or lots of TDD because this will make it easier to catch the generated code's blind spots.
One can imagine that these will be two clearly distinct professions with distinct toolsets.
I actually think that the direct usage of AI will reduce in the system-style group (if it was ever large there).
There is a non-trivial cost in taking apart the AI code to ensure it's correct, even with tests. And I think it's easy to become slower than writing it from scratch.
FWIW, I'm clearly system-style. Given that my current company has an AI product, I'm dogfooding it, and I've found good uses for it, mostly for running quick experiments, as a rubber duck, or for solving simple issues in config files, Makefiles, etc.
It doesn't get to generate much of the code I'm shipping, though.
I agree that non-deterministic isn't the right word, because that's not the property we care about, but unless I'm strongly missing something LLM outputs are very much non-deterministic, both during the inference itself and when projecting the embeddings back into tokens.
I agree it isn't the main property we care about, we care about reliability.
But at least in its theoretical construction the LLM should be deterministic. It outputs a fixed probability distribution across tokens with no rng involvement.
We then sample from that fixed distribution non-deterministically for better performance or we use greedy decoding and get slightly worse performance in exchange for full determinism.
Happy to be corrected if I am wrong about something.
Ah, I realize that I had misunderstood your earlier comment, my apologies and thanks for clarifying!
We're leaving my area of confidence, so take everything I write with a pinch of salt.
As far as I understand, indeed, each layer transforms a set of inputs into a probability distribution. However, if you wanted to compute entirely with probability distributions, you'd need the ability to compose these distributions across layers. Mathematically, it doesn't feel particularly complicated, but computationally, it feels like this adds several orders of magnitude of both space and time.
I guess that the benefit of monoliths in the context is that they (often) live in distinct repositories, which makes it easier for Claude to ingest them entirely, or at least not get lost into looking at the wrong directory.
I‘ve had a similar feeling before Opus 4.5. Now it suddenly clicks with me, and it has passed the shittiness threshold, into the „often useful“ area. I suspect that’s because Apple is partnering with Anthropic and they will have improved Swift support.
Eg it‘s great for refactoring now, it’s often updating the README along with renames without me asking. It’s also really good at rebasing quickly, but only by cherry-picking inside a worktree. Churning out small components I don’t want to add a new dependency for, those are usually good on first try.
For implementing whole features, the space of possible solutions is way too big to always hit something that I‘ll be satisfied with. Once I have an idea on how to implement something in broad strokes, I can give a very error ridden first draft to it as a stream of thoughts, let it read all required files, and make an implementation plan. Usually that’s not too far off, and doesn’t take that long. Once that’s done, Opus 4.5 is pretty good at implementing that plan. Still I read every line, if this will go to production.
Note that in the case of coding, there is an entire branch of computer science dedicated to verification.
All the type systems (and model-checkers) for Rust, Ada, OCaml, Haskell, TypeScript, Python, C#, Java, ... are based on such research, and these are all rather weak in comparison to what research has created in the last ~30 years (see Rocq, Idris, Lean).
This goes beyond that, as some of these mechanisms have been applied to mathematics, but also to some aspects of finance and law (I know of at least mechanisms to prove formally implementations of banking contracts and tax management).
So there is lots to do in the domain. Sadly, as every branch of CS other than AI (and in fact pretty much every branch of science other than AI), this branch of computer science is underfunded. But that can change!
Considering how useful I've found AI at finding and fixing bugs proportional to the effort I put in, I question your claim that it's being underfunded. While I have learned things like Idris, in the end I never was able to practically use them to reduce bugs in the software I was writing unlike AI. It's possible that the funding towards these types of languages is actually distracting people from more practical solutions which could actually mean that it is overfunded in regards to program verification.
FWIW `fmt.Errorf("opening file %s: %w", filePath, err)` is pretty much equivalent to calling `err.with_context(|| format!("opening file {}", path))?` with anyhow.
What `thiserror` or manually implementing `Error` buys you is the ability to actually do something about higher-level errors. In Rust design, not doing so in a public facing API is indeed considered bad practice. In Go, nobody seems to care about that, which of course makes code easier to write, but catching errors quickly becomes stringly typed. Yes, it's possible to do it correctly in Go, but it's ridiculously complicated, and I don't think I've ever seen any third-party library do it correctly.
That being said, I agree that manually implementing `Error` in Rust is way too time-consuming. There's also the added complexity of having to use a third-party crate to do what feels like basic functionality of error-handling. I haven't encountered problems with `thiserror` yet.
> Beyond these concerns, I also don't love enums for errors because it means adding any new error type will be a breaking change. I don't love the idea of committing to that, but maybe I'm overthinking?
If you wish to make sure it's not a breaking change, mark your enum as `#[non_exhaustive]`. Not terribly elegant, but that's exactly what this is for.
> In Rust design, not doing so in a public facing API is indeed considered bad practice. In Go, nobody seems to care about that, which of course makes code easier to write, but catching errors quickly becomes stringly typed. Yes, it's possible to do it correctly in Go, but it's ridiculously complicated, and I don't think I've ever seen any third-party library do it correctly.
Yea this is exactly what I'm talking about. It's doable in golang, but it's a little bit of an obfuscated pain, few people do it, and it's easy to mess up.
And yes on the flip side it's annoying to exhaustively check all types of errors, but a lot of the times that matters. Or at least you need an explicit categorization that translates errors from some dep into retryable vs not, SLO burning vs not, surfaced to the user vs not, etc. In golang the tendency is to just slap a "if err != nil { return nil, fmt.Errorf" forward in there. Maybe someone thinks to check for certain cases of upstream error, but it's reaaaallly easy to forget one or two.
> In Go, nobody seems to care about that, which of course makes code easier to write, but catching errors quickly becomes stringly typed.
In Go we just use errors.Is() or errors.As() to check for specific error values or types (respectively). It’s not stringly typed.
> If you wish to make sure it's not a breaking change, mark your enum as `#[non_exhaustive]`. Not terribly elegant, but that's exactly what this is for.
That makes sense. I think the main grievance with Rust’s error handling is that, while I’m sure there is the possibility to use anyhow, thiserror, non_exhaustive, etc in various combinations to build an overall elegant error handling system, that system isn’t (last I checked) canon, and different people give different, sometimes contradictory advice.
> In Go we just use errors.Is() or errors.As() to check for specific error values or types (respectively). It’s not stringly typed.
errors.Is() works only if the error is a singleton.
errors.As() works only if the developer has defined their own error implementing both `Error() string` (which is part of the `error` interface) and either `Unwrap() error` or `Unwrap() error[]` (neither of which is part of the `error` interface). Implementing `Unwrap()` is annoying and not automatizable, to the point that I've never seen any third-party library doing it correctly.
So, in my experience, very quickly, to catch a specific error, you end up calling `Error()` and comparing strings. In fact, if my memory serves, that's exactly what `assert` does.
> I think the main grievance with Rust’s error handling is that, while I’m sure there is the possibility to use anyhow, thiserror, non_exhaustive, etc in various combinations to build an overall elegant error handling system, that system isn’t (last I checked) canon, and different people give different, sometimes contradictory advice.
Yeah, this is absolutely a problem in Rust. I _think_ it's moving slowly in the right direction, but I'm not holding my breath.
Absolutely. See DeepSeek Prove, for instance. As far as I understand, it's basically a neurosymbolic system, which uses an LLM to write down proofs/code, then Lean to verify them, looping until it finds a proof/implementation that matches the specification, or it gives up.
Create them? Much harder.
reply