At the risk of going slightly off-topic: I think it's interesting you mention "proving programs correct". My hunch is that formal proofs on code are currently too laborious to be useful in most business situations, but that they will become extremely useful as we start letting the machine/"AI" code for us. I might not have spent enough time in this field (so there might be some Dunning Kruger at play) but I think code proofs might be similar enough to Chess/Go that they can be automated, and I think they will be able to add guarantees to computer-generated code so that we can trust it more.