Comment by tialaramex

Comment by tialaramex a day ago

12 replies

> there could even be a cost to correctness

Notice that this cost, which proponents of Zig scoff at just like C++ programmers before them, is in fact the price of admission. "OK, we're not correct but..." is actually the end of the conversation. Everybody can already do "Not correct", we had "Not correct" without a program, so all effort expended on a program was wasted unless you're correct. Correctness isn't optional.

pron a day ago

It isn't optional, and yet it's also not at any cost, or we'd all be programming in ATS/Idris. From those languages' vantage point, the guarantees Rust makes are almost indistinguishable from C. Yet no one says, "the conversation is over unless we all program in languages that can actually guarantee correctness" (rather than one that guarantees the lack of the eighth most dangerous software weakness). Why? Because it's too expensive.

A language like Rust exists precisely because correctness isn't the only concern, as most software is already written in languages that make at least as many guarantees. Rust exists because some people decide they don't want to pay the price other languages take in exchange for their guarantees, but they can afford to pay Rust's price. But the very same reasoning applies to Rust itself. If Rust exists because not all tradeoffs are attractive to everyone, then clearly its own tradeoffs are not attractive to everyone.

The goal isn't to write the most correct program; it's to write the most correct program under the project's budget and time constraints. If you can't do it in those constraints, it doesn't matter what guarantees you make, because the program won't exist. If you can meet the constraints, then you need to ask whether the program's correctness, performance, user-friendliness etc. are good enough to serve the software's purpose.

And that's how you learn what software correctness researchers have known for a long time: sometimes increasing correctness guarantees can have unintuitive cost/benefit interactions that they may even end up harming correctness.

There are similar unintuitive results in other disciplines. For example, in software security there's what I call the FP/FN paradox. It's better to have more FN (false negatives, i.e. let some attacks go through) than more FP (false positives, i.e. block interactions that aren't attacks) because FPs are more likely to lead to misconfiguration or even to abandonment of the security mechanism altogether, resulting in weaker security. So, in software security it's a well known thing that to get better security you sometimes need to make fewer guarantees or try less hard to stop all attacks.

  • Ygg2 18 hours ago

    > It isn't optional, and yet it's also not at any cost, or we'd all be programming in ATS/Idris.

    In a better, saner world, we'd writing Ada++ not C++. However, we don't live in a perfect world.

    > The goal isn't to write the most correct program; it's to write the most correct program under the project's budget and time constraints.

    The goal of ANY software engineer worth their salt should be minimizing errors and defects in their end product.

    This goal can be reached by learning to write Rust; practice makes perfect.

    If GC is acceptable or you need lower compilation times, then yes, go and write your code in C#, Java, or JavaScript.

    • pron 8 hours ago

      > In a better, saner world, we'd writing Ada++ not C++.

      As someone who worked on safety-critical air-traffic-control software in the nineties, I can tell you that our reasons for shifting to C++ were completely sane. Ada had some correctness advantages compared to C++, but also disadvantages. It had drastically slower build times, which meant we couldn't test the software as frequently, and the language was very complicated that we had to spend more time digging into the minutiae of the language and less time thinking about the algorithm (C++ was simpler back then than it is now). When Java became good enough, we switched to Java.

      Build times and language complexity are important for correctness, and because of them, we were able to get better correctness with C++ than with Ada. I'm not saying this is universal and always the case, but the point is that correctness is impacted by many factors, and different projects may find achieving higher correctness in different ways. Trading off fewer use-after-free for longer build times and a more complex language may be a good tradeoff for the correctness of some projects, and a bad tradeoff for others.

      > If GC is acceptable or you

      BTW, a tracing GC - whose costs are now virtually entirely limited to a higher RAM footprint - is acceptable much more frequently than you may think. Sometimes, without being aware, languages like C, C++, Rust, or Zig may sacrifice CPU to reduce footprint, even when this tradeoff doesn't make sense. I would strongly recommend watching this talk (from the 2025 International Symposium on Memory Management), and the following Q&A about the CPU/footprint tradeoff in memory management: https://www.youtube.com/watch?v=mLNFVNXbw7I

      • tialaramex 6 hours ago

        > a tracing GC is acceptable much more frequently than you may think

        Two things here, the easy one first: The RAM trade off is excellent for normal sizes but if you scale enormously the trade off eventually reverses. $100 per month for the outfit's cloud servers to have more RAM is a bargain compared to the eye-watering price of a Rust developer. But $1M per month when you own whole data centres in multiple countries makes hiring a Rust dev look attractive after all.

        As I understand it this one is why Microsoft are rewriting Office backend stuff in Rust after writing it originally in C#. They need a safe language, so C++ was never an option, but at their scale higher resource costs add up quickly so a rewrite to a safe non-GC language, though not free, makes economic sense.

        Second thing though: Unpredictability. GC means you can't be sure when reclamation happens. So that means both latency spikes (nasty in some applications) and weird bugs around delayed reclamation, things running out though you aren't using too many at once, etc. If your only resource is RAM you can just buy more, but otherwise you either have to compromise the language (e.g. a defer type mechanism, Python's "with" construct) or just suck it up. Java tried to fix this and gave up.

        I agree that often you can pick GC. Personally I don't much like GC but it is effective and I can't disagree there. However you might have overestimated just how often, or missed more edge cases where it isn't a good choice.

    • CRConrad 2 hours ago

      > The goal of ANY software engineer worth their salt should be minimizing errors and defects in their end product.

      ...to the extent possible within their project budget. Otherwise the product would — as GP already pointed out — not exist at all, because the project wouldn't be undertaken in the first place.

      > This goal can be reached by learning to write Rust; practice makes perfect.

      Pretty sure it could (at least) equally well be reached by learning to write Ada.

      This one-note Rust cult is really getting rather tiresome.

      • Ygg2 an hour ago

        > The goal of ANY software engineer worth their salt should be minimizing errors and defects in their end product. > > ...to the extent possible within their project budget.

        Sure, but when other engineers discover that shit caused us many defects (e.g., asbestos as a fire insulator), they don't turn around and say, "Well, asbestos sure did cause a lot of cancer, but Cellulose Fibre doesn't shield us from neutron radiation. So it won't be preventing all cancers. Ergo, we are going back to asbestos."

        And then you have team Asbestos and team Lead paint quarrelling who has more uses.

        That's my biggest problem. The cyclic, Fad Driven Development that permeates software engineering.

        > Pretty sure it could (at least) equally well be reached by learning to write Ada.

        Not really. Ada isn't that memory safe. It mostly relies on runtime checking [1]. You need to use formal proofs with Ada SPARK to actually get memory safety on par with Rust.

        > Pretty sure it could (at least) equally well be reached by learning to write Ada.

        See above. You need Ada with Spark. At that point you get two files for each method like .c/.h, one with method definition and one with proof. For example:

            // increment.ads - the proof
            procedure Increment
                (X : in out Integer)
            with
              Global  => null,
              Depends => (X => X),
              Pre     => X < Integer'Last,
              Post    => X = X'Old + 1;
        
            // increment.adb - the program
            procedure Increment
              (X : in out Integer)
            is
            begin
              X := X + 1;
            end Increment;
        
        But you're way past what you call programming, and are now entering proof theory.

        [1] https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Aga...