My answer is already in my previous comment: if you have two formal languages to choose from, you want the one closer to natural language, because it will be easier to see if informal and formal statements match. Once you are in formal land, you can do transformations to other formal systems as you like, as these can be machine-verified. Does that make sense?