[lisper]

Nowadays it's pretty simple:

1. Encode the propositions of your formal system in ascii (or whatever encoding you like)

2. Observe that the resulting bit patterns can be interpreted as numbers, and so the rules of inference of your formal system can be expressed as mathematical operations on those numbers

3. Profit

Goedel had to invent all of that from scratch. On top of that, he had to describe how to actually carry out step 2 without the benefit of a programming language. All he had to work with was raw math. So his encoding was very different from ascii, or anything you are familiar with, because it was "optimized to run on raw math" rather than a digital computer.