Comment by Ygg2

> 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...