Halticopter is an esoteric programming language.
Source code consists of a single Turing machine (we call it ). Input is also a Turing machine (we call it ). Output is a single bit.
Halticopter assumes that does not halt. From that assumption only, it tries to determine whether halts. If the program can conclude that halts, the program outputs and halts. If the program can conclude that does not halt, the program outputs and halts. If the program cannot determine whether halts or not, the program does not halt. If halts, the result is undefined (the program may either output or , or may not halt).
Both source code and input represent Turing machines. The syntax of the Turing machine is the following: it is an array of states separated by new lines and each state is represented either as the "HALT" string (for halting states), or as two groups of 3 space-separated decimal non-negative integers enclosed in parentheses (for non-halting states) - the first group is for the current pointed bit being 0 and the second is for 1. In each group, the first number is 0 or 1 (0 - do not invert the memory bit, 1 - invert the memory bit), the second one is 0 or 1 (0 - go left, 1 - go right), and the third one is the next state (0-indexed). The initial state is the state with index 0. Invalid syntax (either in the source code, or in the input) triggers a syntax error.
Output: undefined (because halts)
(0 0 0) (0 0 0)
Output: If the input is literally the same as the source code, the output is . For any other input, the output depends on the inference rules used to determine whether halts or not (see the "Further research" section).
Input: (a Turing machine that tries to prove a ZF statement starting from the ZF axioms)
Output: If ZF is consistent: if the statement is provable, then the output is , otherwise the output is either , or the program does not halt. If ZF is inconsistent, the result is undefined.
The language does not seem to be precisely defined. The statement "assuming that does not halt, we conclude that..." is pretty vague. The language specification can be improved by defining some formal computable inference rules for deducing whether halts based on the assumption that does not halt (if such rules even exist), but without assuming anything else (such as the consistency of ZF or any other formal mathematical system). The author did not come up with any such rules so far.