From https://www.cl.cam.ac.uk/~djg11/howcomputerswork/

Specification of memory interfaces:

Using some ML-like language, extended with arrays and bounded-range
integers, I give the essence of a formal specification.  


Primary storage:
   type address_t = integer  0 to 2^16 - 1
   type word_t = integer 0 to 255
   method write : address_t * word_t -> unit
   method read  : address_t -> word_t

Secondary storage:
   type blkaddress_t = integer  0 to 2^19-1
   type block_t = array [0..4095] of integer 0 to 255
   method write : blkaddress_t * block_t -> unit
   method read  : blkaddress_t -> block_t option
   method trim  : blkaddress_t -> unit   // Forget a block
   method sync  : unit -> unit           // Blocking flush

Of course, this interface specification says nothing about
the semantics of memory, which are basically what you write
should be what you read back again!  Such a specification
needs to take time into account and whether power has been
turned off in the meantime.

A list of method signatures is one form of API specification,
but sadly, most people neglect to further specify the invocation
order rules: e.g. a file must be opened before it can be closed.

It is critical for database and filesystem design that read returns an
option: a failed write results in either exactly the previously
written data or None (it’s an erasure channel).  A garbled mixture of
new, old and random bits is never returned.

(C) 2021 DJ Greaves.