The paragraph:
The expression assert(0) is a special case; it signifies that it is unreachable code. Either AssertError is thrown at runtime if it is reachable, or a HLT instruction is executed. The optimization and code generation phases of compilation may assume that it is unreachable code.
The problem:
HLT is an implementation, and x86 specific. The language spec should specify intended behaviors first, and implementation as an example if necessary. A description of what HLT does and that it's an x86 opcode should be added if the HLT part remains.