Effects
Many of the operations described in this specification are
effectful. That is, they are
computations that will perform some side effect and are therefore not
directly expressible in Coq's logic. Effectful operations are expressed here as
values of type io. The io F S
type is understood to represent a computation that, when executed, will
perform some side effect and return a value of type S
on success or a value of type F on failure.
The issue of side effects makes it somewhat awkward to describe
the consequences of actions, so the reader is (unfortunately)
required to use good judgement when reading statements regarding
effectful computations. As an example of this problem: "If looking
up an object at path p in the filesystem
succeeds and produces a reference to a file, then looking up the
parent of p must succeed and
yield a reference to a directory". This is obviously true given
normal operating system filesystem semantics. However, looking up
objects in the filesystem is an effectful operation and therefore, the
filesystem could theoretically burst into flames and never yield
the second reference! The reader is more or less expected to
implicitly insert the phrase "assuming that no catastrophic operating
system errors occur" before reading any statement regarding
effectful computations.
The problem could be solved to some extent by specifying an
even more abstract model of the filesystem and then stating that
the effectful computations adhere to properties stated about this
model, but this is certainly not trivial and would probably be
of little practical utility.