1. [theorem proving] A language in which proofs are manipulated and tactics are programmed, as opposed to the logic itself (the " object language "). The first ML was the metalanguage for the Edinburgh LCF proof assistant.
2. [logic] A language in which to discuss the truth of statements in another language.