Why Rust solves a Problem we no longer have – use AI and Formal Proofs instead | Hacker News Reader

Why Rust solves a Problem we no longer have – use AI and Formal Proofs instead

rochuskeller.substack.com

8 pointsRochus7 comments

> You write a `TrafficLight` struct. You use an `enum` for state. You might use a Mutex. The compiler ensures you don’t access the memory of a deleted light. But does it ensure NS and EW aren’t green simultaneously? No. That’s a logic error, not a memory error. Rust saves you from a segfault, but it happily compiles a crash.

But Rust's type system still lets you build a system that covers that logic error. Don't do the naive thing (two lights as enums with states of Red or Green which permits four states, one of which is invalid). Create a four state enum: RG, GR, RR->GR, RR->RG (the third and fourth look superficially the same but indicate which light will become green in the next state transition). You could also do three states (RG, GR, RR) but then you need to track additional state to know which light was green and which will become green, which is neatly encapsulated in the four state machine. There, logic error removed from the program and within Rust's type system.

If you don't want both lights to be red at the same time, then you just do it with two states: RG, GR. Now it's impossible to get into the state where both lights are green because that state doesn't exist and you don't need a guard to prevent it, it literally cannot happen in the code.

That was deliberately just a simple example to give people an impression how the "code" looks which the LLM generates. There is no doubt that you can implement a traffic light with a "traditional" programming approach. The question is rather, why an LLM should produce something which was mostly invented to overcome human weakness, instead of using the much higher potential of this technology. As a programming language author myself I'm interested in the role of programming languages in the age of LLMs; the article represents my conclusions so far.

I picked out that example because it weakened your article. It comes across as a claim that Rust can't help with logic errors, which is false (whether your intent or not that's how it reads). Using bad examples that are easily countered weakens your overall thesis.

Your thesis is interesting, and something I've applied in work (formal methods, or informal-formal methods without the full rigor, to code). But you spend a large amount of the article bashing Rust and its community instead of building up an interesting discussion. I mean, your conclusion section is literally titled "Conclusion: The End of the Cult". Your intent is clear there, to bash a community and language. That's not productive.

As a senior engineer, I am quite alienated by the hype and the completely exaggerated promises that are being made to people. It is precisely such exaggerations that inevitably lead to equally exaggerated counter-movements (such as today's anti-OOP, for example). As long as the community is unable to view technologies objectively, a lot of money and time will be wasted on false expectations. If we don't take a clear stand against this, nothing will improve. I have presented my argument. It consists of more than just a keyword.

> I am quite alienated by the hype and the completely exaggerated promises

And yet here you are writing a post that does that about a different technology. Not exactly the approach I’d expect from a senior engineer.

The individual you responded to did a great breakdown of the bias in your article. You should take it in to account rather than reject it, especially if you want to convince people.

> you are writing a post that does that about a different technology

No, I report based on my experiments and realistic expectations. I don't promise: "just rewrite in Rust and everything is safe, and don't hesitate to spend millions for it". I offer a perspective instead based on proven track records of the technology and present a method how to make it better accessible.

You are once again writing with the same level of bias that was pointed out to you a few comments above.

It is not having the effect you wish to see.

Reply on news.ycombinator.com