I'm looking for a formal language that has the following properties:
- Contains finitely many words (and you can prove it).
- Decidable/recursive (there's a Turing machine that always halts, that can determine whether any given word belongs to the language).
- It's impossible to compute the exact number of words it contains. Meaning, even if you've already found all the words in the language, you can never know if there's another word that you just didn't try yet.
Such a language feels "illegal", but I didn't manage to disprove its existence.