Heheh, it was mostly a reference to my [and mostly others'!] experiments with encoding human languages in a programming language. There are some pretty neat ideas there to explore, like the difference between Subject-Object-Verb (SOV) and Object-Subject-Verb. Or postfix languages (e.g. Forth) mapping to some human languages.

In this particular example, having a subsequent part of an expression rely on prior parts would usually be accomplished at runtime in most languages. But some (like Idris) might allow you to encode the rules in the type system. Thus the rabbit hole.

Ah okay. That's a journey I'm currently also preparing to embark on, though from the other direction: I'm trying to generate "natural" language from program code. I already know it's pretty hopeless, but increasingly I feel like it's not really a choice anyhow, so I may as well finally have a go at it. Let's see :)