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.

Maybe not helpfull, but it made me smile :-)