The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

Okay, but well, Haskell only provides IO by calling into C.
C only supports it by calling into assembly.  Assembly only
supports it by talking to the OS...  :-)

I actually think it's a fun thing for someone to do.

-Greg

On Mar 2, 2010, at 7:00 AM, Adam Koprowski wrote:

>   Dear Bas,
>
> The Ynot library claims to support IO for Coq:
> http://ynot.cs.harvard.edu/
> but this may not be suitable for the shootout.
>   They do, but again: that only works in extracted code (the IO  
> primitives are stated as Coq axioms).
>
>   Adam
>
> --
> Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
> R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris,  
> France]