[Agda] IO design dangers

[Nils Anders Danielsson]

On Mon, Mar 24, 2008 at 4:18 AM, Tristan Wibberley
<tristan at wibberley.org> wrote:
>
>  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.

This would be very nice, but there are two problems:

1) The amount of memory available to the program is typically not
known at compile time. Some properties are inherently dynamic.

2) I expect that keeping track of memory consumption all over the
program will be rather heavyweight, especially if we are talking about
real memory usage and not some abstraction.

Having said that, there are some domains, like embedded systems, where
doing something like this might still be worthwhile because of the
inherent constraints of the domain. Quite a lot of research has gone
into systems keeping track of memory usage, for instance.

-- 
/NAD