Languages designed to specify system. Theoretically, one can execute some specifications.

Executable specification languages include Maude and OBJ3.

----

Also ZedLanguage.

The theory is that the formal language allows one to prove that you have correctly implemented the specification.  The problem is that a specification for a formal language is harder to get right than a normal program.

---

Is BirdMerteensCalculus (see "Functional programming with bananas, lenses, envelopes and barbed wire" and "Bananas in space") a formal language in this sense? HaskellLanguage has a strong grounding in Bird-Merteens theory -- DiegoNavarro