Are Non-Programming golf puzzles allowed?

Question

The name of this Stack Exchange site is "Programming Puzzles and Code golf" but I was wondering if other types of similar golf (not the sport) would be allowed or welcomed for questions. In particular I was thinking about proof golf. Where a statement in Propositional Calculus or First Order Logic is given and the goal is to create a proof using as few axioms of the system.

These types of puzzles are very much like code golfing in practice but they are certainly not code golf or a programing puzzle. I thought it might make a fun one-off challenge, but on the other hand it might be a bit out of scope for this site.

Answer 1

Yes, this is atomic-code-golf

Or, it's what atomic code golf should be. Take a look at

• Multiply with restricted operations
• Build a multiplying machine using NAND logic gates
• Implement an 8 bit adder

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

• A list of fractions
• Text editor instructions
• A bitmap that look like abstract art
• A board for marbles

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.

Answer 2

No.

We're a programming site. Thus, all submissions (and therefore challenges) must involve the use of code*.

^{* A programming language which is executable through a digital interpreter.}