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:
Not really a big fan, because the formalization of DS always left something desired, but I think a big difference with formalization in ULC is that ULC is (mostly) materialist while DS is structuralist.
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.
https://en.wikipedia.org/wiki/Denotational_semantics