Hacker News Reader

Comment by boshalfoshal | Hacker News Reader

I mean Rust definitely has a better tradeoff than Carbon in this case, re readability/verifiability by a person (and sufficiently good internet training data).

I personally think that you _could_ use an LLM to catch these types of boundary case errors without having to port the _entire_ C++ codebase to Rust, but maybe pre-emptively porting to Rust now can catch some of these cases for cheaper than doing a full LLM sweep. Also more cynically, its a good benchmark lol.

I guess if you really believe in curve of LLM capabilities you should just use a language that has the best performance, safety, flexibility, and extensibility, since in the limit few/no people will actually read the code anyway. I think this ends up being Rust.

View on HN

I'm not an expert on this. But isn't it the case that C++ code could have errors that span the entire codebase, like a setup in file A triggered by a bug in file B which is immensely far away on the import graph? A classic would be a use-after-free. To me that's the thing that Rust can help with, even if silly bugs aren't being written by AI.

The other thing is just that rewriting some old human-written codebase in Rust probably immediately catches many bugs. It would be hard to prompt the AI to properly scan for such bugs itself, they're lazy when working in that modality.

I am an expert (in formal methods). LLMs absolutely need more safeguards rather than less. Not because they /need/ them in order to produce functioning code, or even because they produce as many braindead bugs as humans, but because in an era of explosive code quantity, what has become valuable is (assured) code quality.

Going back to C++ would be particularly bizarre to me given that AI is also very proficient at verified languages. Not merely typesafe, but languages comprising their own spec languages such as Rocq and Lean.

I predict that in the next decade: (1) the market will understand the difference between a "code writer" and a "spec writer," with (2) the expectation that the latter is overwhelmingly more necessary than the former in an AI-dominated field, and (3) there will emerge more useful and less mathematically specialized formal verification alternatives to Rocq and Lean, and a filling-out of the tooling gap of between "static typing" and "interactive proof assistant," perhaps in the vein of ACSL-like contract annotations, and (4) there will be a subsequent shift in the traditional curriculum for programmers. Since educational change is slow (and spec writing depends on good coding fundamentals anyway), perhaps (4) is a stretch, but I'm more confident in the first three.

For me personally, when doing development with LLM's, you've won me over towards using safer languages rather than looser ones. Because for one thing, the developer working with an LLM still has to remember to ask it to check for things like memory leaks and security issues. And (as I understand it), LLM's are statistically in the way they work and some level of randomness is always apart of their answer, so there is always a chance they will miss something. Interesting

Could you recommend some lectures/reads about the use of formal methods in LLMs, I'm interested in the area.

Reply on news.ycombinator.com