Comment
Comment by AnthonBerg
A dependently typed language is executed on a computer, therefore it is expressible in assembly code. Like sentences are expressed with words which are expressed with, say, letters. Letters are not sentences, but sentences do guide the expression of letters and vice versa. And sentences can indeed be made out of letters.