Not sure if we are talking about the same thing. If you know why your software is correct, you can write that down as a proof (if you have a language which allo

Not sure if we are talking about the same thing. If you know why your software is correct, you can write that down as a proof (if you have a language which allows you to do that). If you don't know why your software is correct, well, maybe you should not ship it, because maybe it isn't correct. So yes, it is all about push button technology here. If you are willing to put in the work to write down the proof yourself, instead of expecting a magical entity to generate it for you, then it is possible. All the halting problem says is that there is no such magical entity. You will need to know why your software is correct.