[Agda] IO design dangers

[Tristan Wibberley]

Hi folks,

My imagination has flung into action since discovering agda2, it's a
great language.

I'd like to flag a pitfall with future I/O (it seems that it's not yet
supported until the new FFI is released). When doing I/O, operations
like memory allocation can fail. Also, on many operating systems there
are enforced failure conditions (eg, signals). This is one of the
annoying things in Haskell. Failures during computation use this fairly
horrible exception mechanism.

I think, for the proofs in a program to hold, the requirements of the
platform and language implementation must be encoded throughout said
program. So if a program is written to assume a computation will
complete the implementation must allocate all necessary memory (/and
ensure the operating system has not overcommitted/) or, alternatively,
fail to compile. Even then there are cases like sigbus, sigsegv, sigkill
etc (and powerfailure, I suppose, when parts of a computation cannot be
done at compile-time).

It would be really nice for programs that have observable effects to
need to state the failure cases they expect so the implementation can
check what will happen when (and maybe even optimise differently to meet
the expectations).

-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.