[yorwba]

Undecidable languages are formal languages, too, even though there's no Turing machine that can accurately determine for any string whether it is part of the language or not.

A formal language is a set of finite-length sequences (called "words") of symbols from another set (called the "alphabet"). It's essentially a very crude approximation of some strings of letters in an alphabetic writing system forming words in a natural language, while other combinations are just nonsense.

For a given formal language, there don't necessarily have to be any rules governing the words of the language, though the languages used for writing formal proofs are typically more well-behaved.

[pron]

You're talking about formal languages in the context of computer science. Formal languages in the context of logic predate computer science (or could be said to be a direct precursor to computer science). These logic languages are also trivially decidable in the computer-science sense of formal languages, i.e. their set of strings is easily decidable. When we talk of decidability in those languages we ususally mean the decidability of whether a statement is provable or not (using the language's inference rules).

While my explanation of "formal" is meant to be introductory and not entirely precise, that some problem tackled by an algorithm is undecidable does not mean that that problem isn't precisely interpretable by the computer. A Python interpreter doesn't terminate for all inputs (and therefore doesn't decide halting), yet it does interpret all of its inputs precisely.

[schoen]

It does get worse in the sense that there could be languages whose description is incompressible (we can simulate this, assuming hash functions approximate random oracles, by saying "choose a secret key; now the language is 'every string whose HMAC value under that secret key is even'").

If you accept some axiomatic assumptions about infinite sets (that are common in mathematics; I'm not sure exactly what the weakest required axiom is for this), then you can even believe that there are infinite languages that have no finite description at all, very much akin to the commonplace claim that there are real numbers that have no finite description at all. There are formulations of mathematics in which this is not true, but most mathematicians seemingly work in formulations in which it is true.

I even expect that we can probably prove this directly using the powerset operation and diagonalization, which doesn't require particularly strong assumptions about infinities.