Safety by abstract data types + silent truncation:
type PAddr = (PhysPage,POffset)
type PhysPage -- abstract
type POffset = Word12
getPAddr ∈ PAddr → H Word8
setPAddr ∈ PAddr → Word8 → H ()
allocPhysPage ∈ H (Maybe PhysPage)
Safety by abstract data types + run-time bounds checks:
data MemRegion -- abstract
type Offset = Word32
pokeByteOff ∈ Storable a ⇒ MemRegion → Offset → a → H ()
peekByteOff ∈ Storable a ⇒ MemRegion → Offset → H a