So, Eiffel or Ada and TLA+

That’s what the article is about.

I'm writing one of these, I'll post it on HN next year. The key to a language for LLMs is: make sure all the context is local, and explicit. If you have functions, use parameters for arguments instead of positions. If you have types, spell them out right there. Also, don't use too many tokens, so keywords are out. And that's just a start.

I think the ideal language for LLMs will look more like APL than C.

Idiomatic Rust prevents many classes of logic errors. Just having proper sum types eliminates many (perhaps most) common logic errors.

> Rust doesn't prevent programs from having logic errors.

Like everything around Rust, this has been discussed ad nauseam.

Preventing memory safety bugs has a meaningful impact in reducing CVEs, even if it has no impact on logic bugs. (Which: I think you could argue the flexible and expressive type system helps with. But for the sake of this argument, let's say it provides no benefits.)

technically true but so what?

https://security.googleblog.com/2025/11/rust-in-android-move...

That team claims that not having to deal with memory bugs saved them time. That time can be spent on other things (like fixing logic errors)

All kinds of drugs produce unwanted risks and side effects if abused, so let's abuse crystal meth! Cannabis isn't going to save you.

> Rust doesn't prevent programs from having logic errors.

Nobody ever claimed that. The claims are:

1. Rust drastically reduces the chance of memory errors. (Or eliminates them if you avoid unsafe code.)

2. Rust reduces the chance of other logic errors.

Rust doesn't have to eliminate logic errors to be a better choice than C or assembly. Significantly reducing their likelihood is enough.

This is objectively wrong.

You can't get a gutter ball if you put up the rails in a bowling lane. Rust's memory safety is the rails here.

You might get different "bad code" from AI, but if it can self-validate that some code it spits out has memory management issues at compile time, it helps the development. Same as with a human.

Modern medicine can't prevent or cure all diseases, so you might as well go back to drinking mercury then rubbing dog shit into your wounds.

Modern sewers sometimes back up, so might as well just releive yourself in a bucket and dump it into your sidewalk.

Modern food preservation doesn't prevent all spoilage so you might as well just go back to hoping that meat hasn't been sitting in the sun for too many days.

> Rust doesn't prevent programs from having logic errors.

Sure, but it prevents memory safety issues, which C doesn't. As for logic bugs, what does prevent them? That's a bigger question but I'd suggest it's:

1. The ability to model your problem in a way that can be "checked". This is usually done via type systems, and Rust has an arguably good type system for this.

2. Tests that allow you to model your problem in terms of assertions. Rust has decent testing tooling but it's not amazing, and I think this is actually a strike against Rust to a degree. That said, proptest, fuzzing, debug assertions, etc, are all present and available for Rust developers.

There are other options like using external modeling tools like TLA+ but those are decoupled from your language, all you can ever do is prove that your algorithm as specified is correct, not the code you wrote - type systems are a better tool to some degree in that way.

I think that if you were to ask an LLM to write very correct code then give two languages, one with a powerful, express type system and testing utilities, and one without those, then the LLM would be far more likely to produce buggy code in the system without those features.

I guess there is a reason why Linux kernel accepts Rust not Haskell.

Can you elaborate? What is it about Haskell that makes it better?

I would think Lean and other formal languages are the real gold standard.

But none of them really have enough training data for LLMs to be any good at them.