What I want I'd : we have used contracts in the tall world. This is what works and doesn't. This catches a lot of bugs for little work. This looks the same but results in false positives. This is a lot of work for few bugs.

Of course since I don't know what works I'm guessing, but that type of thing.

Consult a real lawyer if this matters to you. The above is my understanding of the law, but I'm not a lawyer and different countries have slightly different laws.

However some court will eventually tell them no. Big tech has gotten away with a lot, and courts try to be hands off. However eventually the power rests with the government not big tech and so when the courts decide to act they can strike much harder than big tech.

It isn't reasonable to expect downstream (i.e. Debian) to fix warnings but developers generally do for code they maintain.

Are they struggling with a 4 way stop - or did they just prevent a crash because someone else you didn't even notice just did something stupid? That someone else might be you not knowing you even did something wrong!

Of course I have no idea how you drive, how much training you have or the other important details. The above shouldn't be taken as a personal attack on your actual driving. The attack does fit every other driver I know though (including me - though it is hard to be honest about my own failings)

My sump pump hadn't run at all to my knowledge (I hear it so I think I'd know but maybe I was always gone or sleeping) for several years, but the power went out in a big rain storm and so the one time I needed it, it didn't run. (my old generator didn't kick on like it is supposed to, but I'm not sure if that circuit is wired to the generator anyway)

Israel has a lot of enemies that going against them. Which is why they have incentive to be good at this - to attack back. Corporate attempts are just ways to make money.

I'm going to stay out of the political issue of what any actor should do.

I think the right answer is in the header, and in turn that means someone needs to answer your objection - how do you avoid long compiler times? I suspect modules is a large part of the answer, which means the guide/talk will also be how to make modules work in the real world. Remember though, that is all guesses I wouldn't be surprised if I'm wrong.

Contracts also allow a solver to say "I can't prove this messy function, but I can at least prove everything around it". Which is to say if we prove the precondition is met, and if we assume the post conditions are met, we can prove everything else despite the messy parts we can't do. This at least lets us know where the messy code is.

Contacts are also a guaranteed syntax. Runtime checks provide no way for tools to know if the condition is expected to never happen - this is a bug; vs this is a normal user error we need to check for. A contract means theorem provers can find code paths where a bug could happen - of course we don't have theorem provers for C++, but this is seen as a requirement to get them.

I think training could help. However I don't think it will. People think they are good enough and will write down answers to pass the test. Maybe if the training was mandatory behind the wheel with failure meaning you lose your license - but the voters won't stand for that.