@darkuncle@infosec.exchange
You are speaking specifically about *mathematical* proofs.
Not all proofs are.
For example - we prove a case in court. In English. And yes, there's some jargon to help make things more precise, but the soul of the proof isn't the words, it's the logic.
But we've moved goalposts. We're not talking about proofs. We're talking about unambiguous instructions. A formal language can certainly help there, but my assertion is simpler - a more intelligent listener (or "interpreter") is even better.
I can write the same logic in any sufficiently complex language - assembly, COBOL, BASIC, Pascal, Perl, Python. And it *generally* gets easier as the languages get more complex, because they can succinctly encapsulate higher level constructs without having to enumerate the details. Sorting, for example, becomes easier and easier as the language gets more recent.
COBOL as an attempt to make programming resemble English, on the theory it would allow non-programmers to program. It turns out that's not true - you need a programmer's "mindset" to write code, to be able to work out what you want done with sufficient rigor to get the computer to do it.
I submit to you: talking to the AI, in English, with sufficient programming mindset rigor - is the next step. I can produce the same artifact by either writing python directly or instructing an AI - but the context the AI embodies about code and coding and best practice and so on means I can do it faster and easier, significantly so - which leaves me more time for the other important bits, like design and security and testing.
Is it perfect? No. In particular, the AI can't fill in for a lack of that programming, logical mindset. Garbage in, garbage out. You need to learn *how* to talk to an AI about coding, in much the same way you needed to learn Perl - or you're going to have a poor experience. And I fear we have folks missing that step. But perfection was never the promise.
You hear a lot of people bag on AI. For lots of reasons - many good. But you know what you don't hear? People who have used it for coding and abandoned it as useless. Because - it's not.
