This is a bit backwards. Formal systems engineering is rooted in defining problems in natural language. The programming languages are normally used for defining the solutions, not the problems. Even if you're taking about TDD, the executable tests are still derived from natural language test case specifications.