> He clearly hasn't proven anything about his code.

Is that a bad thing? It seems like many people are able to write software that works well and gets the job done without "proving anything" about their code in the way you're describing. Personally, I'm fine with not proving anything if I can deliver quickly and everything works, but I'd like to be convinced otherwise if there's real value there.

Formal verification of code has been the elusive Graal seeked by many for now a few decades.

It’s a mirage to which many have succumb but like in the desert most died of thirst trying to catch it.

For basic infrastructure such as compilers and standard libraries (at least of data structures and algorithms), not providing proofs of correctness is outright criminal.

It's not though is it... You know, because there aren't actual laws about it.

Let's try not to make inflammatory statements.