While there is certainly quite a bit of truth to what you say, I have a few counter arguments:
> 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.
For my purpose I don't need to get back to the original source, no.
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'm wondering if it would rather make more sense to emulate a CRT with a video projector and some shutter device (maybe a fan?) in front. Has anyone tried that yet?
At least for user space usage, I'm not sure a new kernel thing is needed. Quite a while ago I have implemented a user space (single producer / single consumer) ring buffer, which uses an eventfd to mimic pipe behavior and functionality quite closely (i.e. being able to sleep & poll for ring buffer full/empty situations), but otherwise operates lockless and without syscall overhead.
> 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.