> same order of magnitude as the code implementing it
I believe mathematically formulating what an algorithm should do is very often orders of magnitue simpler than implementing it. As we know from the halting problem, it is easy to specify what the algorithm should do, but it is provably impossible to implement such an algorithm, so there the ratio of complexity is infinite ;)
Also, the huge advantage of a specification is that it is much more compositional than actual code. As the article states, one can just specify (and verify) that the code never crashes totally independent from what the code otherwise should be doing. So one can easily look at each part of the specification and understand why it is a desirable property piece by piece, in much larger isolation than the monolithic totality of the code.
Even more, with a formal specification one can (and probably should, when it gets too compilcated) verify by proof that the spec is internally consistent, i.e. that no part contradicts the requirements of another.
The gcc part is only relevant with regards to what dialect of assembler I need to parse. If I go that route, I'd write a parser for the GNU assembler, and that would of course work with any code in that dialect, regardless from which compiler it came from (I haven't checked whether other compilers can produce GNU assembler though).
I'd like to do some statistics over the machine code gcc generates, such as a histogram of used instructions, average volatile/preserved registers usage of functions etc. For now just x86_64 SysV-ABI would be enough.However I'm not aware of any pre-existing tool that lets me easily do this. The options I currently see are either make gcc output assembly and write a parser for the GNU Assembler...