Isn't it today/wouldn't it be in the close future relatively trivial to port most of the already formalized results between languages with help of LLMs?