I disagree slightly here. There may be one (1) dominant formal language that's used as the glue code that gets run on machines and verified, but it will have numerous font-end languages that compile into it, for ease of typing and abstraction/domain fit.