MATH.12:8 - Common Anti-Patterns and How to Avoid Them

Failure	Repair
Read “there exists” as an available obtaining operation	Recover the witness-producing step or name the construction still needed.
Turn an unspecified disjunction into an executable branch	Supply a decision and return its case tag with the relevant data.
Change a witness that depends on x into one fixed witness for every x	Keep the input parameter and the statement’s quantifier order.
Project program data from a formal proposition that does not expose it	Use an appropriate data-bearing construction or obtain the value by another supported method.
Infer termination from a program type that permits general recursion	Establish termination for the actual computation or retain its partial scope.
Replace one calculation by repeated calls while forgetting changing state or cost	Retain shared results and restore the state needed by the mathematical model.