3 ms·
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 t
by samvher 6y ago
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.
- gpanders 6y agoIf the code proofs are automated, then how do you prove the proof? Pardon my ignorance, but I’m being sincere. I don’t know much about this field.
- samvher 6y agoWhen it comes to formal proofs of code, once you have a proof it is generally straightforward to verify (in the same way that you could for example evaluate a boolean expression). The problem is in finding the proofs - that's what requires labor and intelligence. So the way I imagine it would work, is you tell a programming system which conditions the code it's going to generate should satisfy, and then it generates the code + proofs that it satisfies those conditions. It might be trickier than I imagine though (e.g. for Chess/Go the reinforcement signal might be more suitable for learning than what you'd find with proofs). If you want to know more about proofs you might be interested in the series "Software Foundations" (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/).