The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Marko Malikoviæ wrote:
> I'm trying to find some function for generating random (pseudo-random)
> numbers in Coq. It seems that it doesn't exists. Am I right?
> If it doesn't exists than I need some seed state. But, I don't see some
> time (or simmilary) function in Coq.
>   

Every Coq function is pure.  It is impossible to write a function of 
type, e.g., [unit -> nat] that returns different values on different 
calls.  Thus, there can exist no equivalents of C rand() or time(); 
assuming such a function exists leads to a contradiction.

You can still thread a time or random number seed through a program as 
an explicit argument/return value, though.