Examples of Turing complete formal systems include the following (along with the person credited for inventing the system, and date of seminal paper describing it, where applicable, or known):

That is, it is possible for any instances of these systems to simulate and be simulated by any of the others. The fact that all of these formal systems for computation can generate only recursively enumerable languages and calculate partial recursive functions lends credence to the Church-Turing Thesis.

These various Turing complete formal systems have become the basis for various styles of programming and associated programming languages. For instance the register machine model has become the main model behind which nearly all machine languages for nearly all modern microprocessors are based. The lambda calculus is the basis for all functional languages, and the related combinator logic is used for some implementations.