Why Rust solves a Problem we no longer have – use AI and Formal Proofs instead(rochuskeller.substack.com)
3 pointsby Rochus4 hours ago1 comment
  • Jtsummers4 hours ago
    > 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.

    • Rochus3 hours ago
      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.
      • 3 hours ago
        undefined
      • Jtsummers3 hours ago
        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.

        • Rochus3 hours ago
          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.