Grounding programming languages in mathematics like this is essentially the goal of Strachey and Scott's denotational semantics, which has been very influential in programming language theory:
So the initial formalization into ULC can be automated - if you have semantics of your language already implemented as an interpreter in another language, you can use this as a starting point.
With DS - I am not sure. I feel most people who build new languages don't provide DS specification.