effective/constructive/algorithmic probability theory What sort of "alternative" probability theories are out there in which the methods of proof are inherently constructive?
I know of a number of theorems that say that if you take an infinite sequence of i.i.d. random variables of thus-and-such a kind (let's say that they're fair bits, for definiteness), and use them in a specified fashion to generate a sequence of combinatorial objects of a particular sort, and rescale those combinatorial objects in a time-dependent fashion, then the rescaled objects converge to some sort of limit object with probability 1.  However, the proofs that I know are ineffective, in the sense that the proofs don't give you a way to construct any particular infinite sequence of bits such that, if you use them as described above, the convergence occurs.
Well, sort of.  In each case of this situation occurring, there's a way to "cheat" by using the theorem itself to guide the choice of bits; you can just choose your bits to have the behavior that you're trying to prove.  Is there some principled way to rule out such "cheating"?  When it comes to cheating, I believe that "I know it when I see it", but I don't know how to formulate a precise definition of cheating that captures my intuitions.
A web search turned up a talk on "Applications of Effective Probability Theory to
Martin-Lof Randomness" (http://www.loria.fr/~hoyrup/icalp_slides.pdf), which is one example of the kind of theory I mean.  Are there others?
 A: A recent paper that gives the sort of effective result you're after is Freer and Roy's Computable exchangeable sequences have computable de Finetti measures. From their introduction:
The classical result states that an exchangeable sequence of real random
variables is a mixture of independent and identically distributed (i.i.d.) sequences
of random variables. Moreover, there is an (almost surely unique) measure-valued
random variable, called the directing random measure, conditioned on which the
random sequence is i.i.d. The distribution of the directing random measure is
called the de Finetti measure.
We show that computable exchangeable sequences of real random variables
have computable de Finetti measures. In the process, we show that a distribution
on $[0,1]^\omega$ is computable if and only if its moments are uniformly computable.

Like the work of Hoyrup and Rojas that you point to in your question, this paper operates under the type-2 theory of effectivity (TTE) framework for computable analysis (for more on which see e.g. Weihrauch's text Computable Analysis), though unlike Hoyrup and Rojas' work, notions from algorithmic randomness are not employed here.
I know you said you're after a theory for ruling out the "cheating" you describe. Really, there's nothing special about probability theory here, and I think computability theory itself (coming in this setting in the guise of TTE) is already what you want in order to determine when "cheating" is generally necessary. It just boils down to proving, for a given theorem, either (1) you can always compute the conclusion data from the hypothesis data, or (2) there are instances where it cannot be computed.
The Freer and Roy paper is an instance of the former; an instance of the latter can actually be found in a more recent paper of theirs, with Nate Ackerman, on conditional probability. From the abstract: "We ... show that there are computable joint distributions with noncomputable conditional distributions, ruling out the prospect of general inference algorithms, even inefficient ones. Specifically, we construct a pair of computable random variables in the unit interval such that the conditional distribution of the first variable given the second encodes the halting problem."
