The how that matters must be part of your spec, of course. It is turtles all the way down, but the point is that apart from the top turtle, all the other turtles will be AIs. That's a big difference.
Just the step from "program" => "spec" is already a big one. So big, that it is rarely done today. Test-driven development is an attempt at this, but the problem is that tests cannot truly verify a spec. Proofs can. Of course, you can combine tests and proofs, for example proofs for correctness, tests to make sure other measures like speed and cost are sane. But if you want to be absolutely sure, you will need to replace all tests by proofs.
