Or, it's what atomic code golf should be. Take a look at
All of them define a mini-language by listing a limited set of allowed operations, and ask for a task to be done in as few of these operations as possible.
In the same vein, one could have a challenge to construct a regular pentagon in as few ruler-and-compass operations, writing out the operation like "draw a circle with the given point and the current radius", "mark a point at the intersection of two lines", and so on. One could write an interpreter for this language, where each operation is a code instruction, the current picture is the program state, and so on. The result is a challenge like code golf, except that:
- All submissions must be in the given invented language
- Rather than minimizing characters, one minimizes operations
Your first reaction might be, "but that's not a programming language, it's geometry!". But why? Perhaps the NAND gate language feels like programming because logic gates happen to be what computers use. It's just association. We already use esoteric languages where a "program" is
And anyone is free to make their own language. Using weird languages is a point of pride in the community. So let's not call something "not programming" for not looking like a typical programming language.
Formal proofs, which OP used as an example, have a particularly close relationship to programming. The Curry-Howard correspondence, aka the proofs as programs interpretation, gives a formal mathematical equivalence between proofs and programs. A challenge to prove a statement in a formal system could be rephrased as writing a program that instantiates a given type.