Abstraction for limited memory access
A Safe Interface:
Readable ∈ Addr → Prop Writable ∈ Addr → Prop peek16 ∈ (a∈Addr) → Readable a → H Word16 poke16 ∈ (a∈Addr) → Writable a → Word16 → H ()
Primitives to declare what constitutes safe memory access:
Unsafe.readable ∈ (a∈Addr) → Readable a Unsafe.writable ∈ (a∈Addr) → Writable a
Dependent types! Propositions as Types!
Let's us talk about values (memory addresses) at the type level.