On today's HN with this thread is "the hole in mathematics".
It is directly germane to what you are talking about.
In the process of formalizing axiomatic math, 1+1=2 took 700 pages in a book to formally prove.
The point about assembly is more or less correct. The process of de-abstracting is going to be long and probably not that clear in the end.
I understand what you mean: the assembly commenter is correct, you'll need to actually execute the program and reduce it to a series of instructions it actually performed.
Which is either an actual assembly, or a pseudo-assembly instruction stream for the underlying turing machine: your computer.
I really need you to introduce you to Jester, my toy functional programming language. It compiles down to pure lambda calculus (data structures are implemented with Scott-Mogensen encoding) and then down to C that uses nothing but function calls and assignments of pointers to struct fields. The logic and arithmetic are all implemented in the standard library: a Bool is a function that takes 2 continuations, a Byte is 8 Bool, an Int is 4 Byte, addition uses the good old ripple-carry algorithm, etc.
Reading the disassembly of the resulting program is pretty unhelpful: any function consists entirely of putting values from the fields of the passed-in structures into the fields of new structures and (tail)calling another function and passing it some mix of old/new structures.
