I think the point that LLMs should enable effective translation between different formalisms is a good one. So I don't see the choice as being a big issue. This is especially the case here because to a large extent the translations can be checked automatically.