It’s neither. I’m claiming you need more than just a theorem prover’s mental skills to accomplish the task. If you think you can formulate the specification in formal mathematical logic, so that you do only need a theorem prover to accomplish the task (and also a list of possible programs), then go ahead. I’d be excited if you succeeded.
Can’t tell if this is a job offer or an argument of the form “I tried this and failed therefore it is impossible”
It’s neither. I’m claiming you need more than just a theorem prover’s mental skills to accomplish the task. If you think you can formulate the specification in formal mathematical logic, so that you do only need a theorem prover to accomplish the task (and also a list of possible programs), then go ahead. I’d be excited if you succeeded.