druck  wrote:
> The use of ambiguous instructions to indicate parenthesis, or anything
> else, would have been useless, or even worse than useless. Similarly
> even when the full source code is available, you do not rely on the
> comments, as they are often out of date or just wrong. There is only one
> thing that tells you want the code is doing, and that is the code itself.

And that only tells you half of the story.  The reason I pointed to the work
of Alastair Reid and others is that to reason about what the code is doing,
you have to know what instructions mean.  That is surprisingly tricky.  Even
simple arithmetical operations get difficult when you start talking floating
point, and then there's questions about accelerators, system control,
caches, MMUs, system on chip components...

The pathways from ISA descriptions to formal models allow reasoning about
what the program does to the state of the system, whether that is the
desired outcome and whether it is well-defined for all inputs.  They are
very handy in finding architectural bugs.

Theo

--- SoupGate-Win32 v1.05