You are right in that the code (or the formal model) alone isn’t sufficient, in that it doesn’t specify the context, requirements, design goals and design constraints. The formal and the informal level complement each other. But that’s also why it’s necessary to think at both levels when developing software. Withdrawing to just the informal level and letting LLMs handle the mapping to the formal level autonomously doesn’t work.

That being said, even model-based design (MBD) has largely been a failure, despite it being about mapping formal models to (formal-language) program code.

architecture is about the choices you will regret in this future if you get wrong today. You will regret not having testable code so tdd isn't bad - but that is not the whole storyand there are many things you will regret that tdd won't help with.

there is the famious bowling game tdd example where their result doesn't have a frame object and they argue they proved you don't need one. That is wrong though, the example took just a couple hours - there is nothing so bad in a a two hour program you will regret. If you were doing a real bowling system with pin setters, support for 50 lanes and a bunch of other things that I who don't work in that area don't even know about - you will find places to regret things.