Constraint programming would be extremely powerful. They aren’t a silver bullet, but they would make a ton of hard problems a lot easier. Particularly when it comes to proving whole-program correctness properties like “does not use more than X memory”.
For example, when a human programmer is designing a public key cryptosystem, they’re trying to satisfy properties like “there is no tractable Turing Machine that takes a public key as input and outputs the corresponding private key with non-negligible probability”. Doing that is really, really hard compared to just writing down what we want to satisfy.
It’s true that it would need to be insanely powerful. Even clever humans haven’t managed to prove that one-way hash functions exist (though we know a function that is one-way if and only if they exist...).
Note theorem proving is isomorphic to programming. Even if it wasn’t quite so equivalent, you could just ask for a constructive proof of a program satisfying whatever and the proof would contain the program.
Constraint programming would be extremely powerful. They aren’t a silver bullet, but they would make a ton of hard problems a lot easier. Particularly when it comes to proving whole-program correctness properties like “does not use more than X memory”.
For example, when a human programmer is designing a public key cryptosystem, they’re trying to satisfy properties like “there is no tractable Turing Machine that takes a public key as input and outputs the corresponding private key with non-negligible probability”. Doing that is really, really hard compared to just writing down what we want to satisfy.
But that’s going to take an insanely powerful theorem-prover. Also, this is more the theorem-proving end than automated program end.
It’s true that it would need to be insanely powerful. Even clever humans haven’t managed to prove that one-way hash functions exist (though we know a function that is one-way if and only if they exist...).
Note theorem proving is isomorphic to programming. Even if it wasn’t quite so equivalent, you could just ask for a constructive proof of a program satisfying whatever and the proof would contain the program.