[plt-scheme] Expressivity gap between formal methods and PL's

To what extent can a programming language (of the right type)
replicate the expressivity of formal languages.

It seems to me that if an organisation is going to deploy formal
methods  then it would always make sense to do an implementation in a
language that as far as possible retains the same expressive
constructs. I do not see the sense in going straight to an
implementation language (like the one that begins with a J) for such
systems. Well ok people may say performance, or the ability to recruit
staff, but I argue that  it would still seem worth creating an
executable in a language capable of expressing similar formalisms  as
an  oracle for testing your final implementation.

Second question. What is the difference between formal languages and
modelling languages (is the answer the degree of formalism?).