That's not a very helpful response. Unless the code is compiled to native machine code and is all inlined, this won't help one bit.

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 :-)