  Program logics are a powerful formal method in the context of program
verification. Can we develop a counterpart of program logics in the context of
language verification? This paper proposes language logics, which allow for
statements of the form $\{P\}\ \mathcal{X}\ \{Q\}$ where $\mathcal{X}$, the
subject of analysis, can be a language component such as a piece of grammar, a
typing rule, a reduction rule or other parts of a language definition. To
demonstrate our approach, we develop $\mathbb{L}$, a language logic that can be
used to analyze language definitions on various aspects of language design. We
illustrate $\mathbb{L}$ to the analysis of some selected aspects of a
programming language. We have also implemented an automated prover for
$\mathbb{L}$, and we confirm that the tool repeats these analyses. Ultimately,
$\mathbb{L}$ cannot verify languages. Nonetheless, we believe that this paper
provides a strong first step towards adopting the methods of program logics for
the analysis of languages.
