We have these tools that we use to write formally correct documents.

They're called programing languages, and a deterministic algorithm translates them to machine code.

Are we sure English and a probabilistic algorithm is any better at this?

I actually hate AI in my core, to the point that if it gets too much more advanced I'll likely be in existential crisis, so don't attack me on those grounds. Given it exists, I'm going to find what's good about it though. I do think the problem of AI existing has to be confronted. Maybe one solution is what the human does is produce specs like the HTML 5 one, and what the AI does is implement it in software.