> I'd feel a lot more comfortable in the prospects of AI if their big boosters weren't so gung-ho about it replacing absolutely everything. Compilers (and by extension decompilers) are one of the areas where we have the ability to have formal proofs of correctness [1]--and the fact that AI people seem to be willing to throw all of that away in favor of their maybe-correct-but-does-it-really-matter-if-it's-not tools is extremely distressing to me.

God yes. These people are infuriating; it's as if they've abandoned the concept of provable correctness, or never understood it in the first place, and replaced it with "looks good enough to me on a few examples". Some sort of gambler's fallacy where if you get a right answer once it doesn't matter how many wrong answers you get.