"Simpler" statements equivalent to Con(PA) or Con(ZFC)? Given any reasonable formal system F (e.g., Peano Arithmetic or ZFC), we all know that one can construct a Turing machine that runs forever iff F is consistent, by enumerating the theorems of F and halting if it ever proves 0=1.
However, what interests me here is that the "obvious" such Turing machine will be an extremely complicated one.  Besides the axioms of F, it will need to encode the symbols and inference rules of first-order logic, which (among other things) presumably requires writing a parser for context-free expressions.  If you actually wrote the Turing machine out, it might have millions of states!  Even in a high-level programming language, the task of writing a program that enumerates all the theorems of ZFC is not one that I'd casually give as homework.
Notice that this situation stands in striking contrast to that of universal Turing machines, which we've known since the 1960s how to construct with an extremely small number of states (albeit usually at the price of a complicated input encoding).  It also contrasts with the observation that very small Turing machines can already exhibit "complicated, unpredictable" behavior: for example, the 5th Busy Beaver number is still unknown, and it seems like a plausible guess that the values of (say) BB(10) or BB(20) are independent of ZFC.
Thus my question:

Is any "qualitatively simpler" class of computer programs known, which can be proved to run forever iff ZFC is consistent?  Here, by "qualitatively simpler," I mean doing something that looks much more straightforward than enumerating all the first-order consequences of the ZFC axioms, but that can nevertheless be proved by some nontrivial theorem to be equivalent to such an enumeration.  Feel free to replace ZFC by ZF, PA, or any other system to which Gödel's Theorem applies if it makes a difference.

This question is clearly related to the well-known goal of finding "natural" or "combinatorial" statements that are provably independent of PA of ZFC, but it's not identical.  For one thing, I don't demand that your statement have any independent mathematical interest---just that the computer program corresponding to your statement be easier to write than a program that enumerates all ZFC-theorems!
One concrete goal would be to find the smallest n for which you can prove that the value of BB(n) (the nth Busy Beaver number) is independent of ZFC.  (It's clear that BB(n) is independent of ZFC for all n≥n0, where n0 is the number of states in a Turing machine that enumerates all ZFC-proofs and halts if it proves 0=1.)
As a first step, though, I'll be delighted to learn of any theorem that simplifies the task of writing proof-enumerating programs.  (Even if the programs are still expressed in a high-level formalism, and are still horrendously complicated when compiled down to Turing machines.)
 A: The discussion in the comments has helped clarify your question for me.  I believe that it is closely related to the following remark by Harvey Friedman:

I am convinced that trying to take consistency statements like Con(ZFC +
  measurable cardinals) or Con(ZFC + rank into itself), Con(ZF + inaccessible
  rank into itself), etc., and force them into smaller and smaller Turing
  machines not halting, with demonstrable equivalence in an extremely weak
  system, is an open ended project, in the practical sense, that will create a
  virtually unlimited opportunity, in the practical sense, for a stream of
  ever and ever deeper mathematical ideas. Ideas that could come from
  unexpected sources, ideas that could have independent deep ramifications,
  ideas that -- well who knows what to expect. The benchmark is completely
  clear - how many quadruples? At the very least, deep ideas about set theory
  and large cardinals, but probably much more diverse deep ideas about, well,
  the unexpected. Any branch of mathematics whatsoever might prove useful, or
  even crucial, here. Whereas, we don't think that "any branch of mathematics"
  might be useful in logic problems, normally. This is different.

Other relevant postings from the FOM archives may be found here and here.
So Friedman's work, that Andres Caicedo alluded to in the comments, is probably the closest thing to what you want.  I don't know of any other people who are working actively on this kind of project.
As a side remark, I believe that your intuition is correct that there is some kind of intrinsic "complexity" to the statement "ZFC is consistent," and roughly speaking it is because the totality of mathematical knowledge is a "complex" entity.
A: How about this:  As discussed in 
Does anyone know a polynomial whose lack of roots can't be proved?
there is a polynomial in several variables that has an integer root iff ZFC is inconsistent.
In other words, if the polynomial has $n$ variables, you can enumerate all $n$-tuples of integers and plug them into the polynomial until the result is 0.
Since ZFC is consistent (as we all know), the computer program will run forever.  
A: Maybe I understand the question wrong, but I think you should specify the logic in which the equivalence is proven. This is a little bit similar to relative consistency. Then you have three logics. The two logics that you compare and the logic in which you prove the relative consistency.
If your logic that proves the equivalence, can prove Con(PA), then the equivalent Turing machine is quite simple. Just a Turing machine that runs forever.
About the question itself. One reason why making a program that enumerates the theorems is hard, is because a logic is non-deterministic (you have choices in the axioms and inference rules you use) and a programming language (and a Turing machine) is deterministic. The task becomes much easier if you take a non-deterministic language.
To show that with a simple example. Take the last theorem of Fermat. To encode that as a halting problem, you have to diagonalize over a, b, c and n. This require some amount of coding. However, in a non-deterministic language, you just take a, b, c and n non-deterministic. A much simpler program.
Finally, the tricky part of programming the axioms and inference rules of a logic, is the variable substitution and the problem when variables are used multiple times. I think it should be possible to get fully rid of variables, which makes it easier to program, but less readable for humans.
Lucas   
