Peek and Poke again

Primitives for memory access

• type Addr = Word32 peek16 ∈ Addr → H Word16 poke16 ∈ Addr → Word16 → H ()
• Unsafe! Allows any memory location to be overwritten.
  • With unrestricted use, no interesting run-time invariants can be guaranteed.