Having a formal ISA specification - What does correctness mean?

Does this always mean that a program can be correct in regard to that spec or is there any correctness of the spec itself ?

An ISA spec says how a processor should behave. A processor either conforms to such a spec (behaves exactly like the spec says it should), or it doesn’t (behaves differently in some situations).

ISA has nothing to do with correctness of programs. If a processor conforms to its ISA spec then all programs will behave as they should behave according to the spec, both correct and incorrect programs. If a processor does not conform to the ISA spec then programs can behave different from how they should behave.

A spec cannot be wrong, by definition. It can be nonsensical (like if the spec says that an “add” instruction should subtract, but it’s never wrong.

Reasons for having an ISA spec:

• Instructing the team that designs the processor.

• Instructing the team that writes test code to test the processor for conformance.

• Instructing the team that writes a simulator for the processor which can be used before processors are available.

• Instructing teams that write compilers for this processor.

• Instructing support teams who handle customer complains about the processor behaviour, so they can check that the processor conforms to the spec.

StackExchange Computer Science Q#114629, answer score: 3