## Stream: Is there code for X?

### Topic: random number generator

#### Kenny Lau (May 15 2020 at 21:26):

Do we have an RNG? Presumably it will take in the system time in some way or another

#### Chris Hughes (May 15 2020 at 21:27):

I remember seeing one somewhere in core I think.

#### Kenny Lau (May 15 2020 at 21:27):

there's io.rand in https://github.com/leanprover-community/lean/blob/master/library/system/io.lean

#### Kenny Lau (May 15 2020 at 21:27):

but it doesn't use the system time

#### Reid Barton (May 15 2020 at 21:27):

You could read bytes from /dev/urandom (probably)

#### Kenny Lau (May 15 2020 at 21:30):

how do you read a file?

#### Chris Hughes (May 15 2020 at 21:31):

It's an actual function, so you can prove theorems about it if you want

#### Kenny Lau (May 15 2020 at 21:32):

I just want random numbers for a programming kata

#### Kevin Buzzard (May 15 2020 at 21:37):

Kenny Lau said:

I just want random numbers for a programming kata

I would recommend 37

#### Jalex Stark (May 15 2020 at 22:05):

Kenny Lau said:

I just want random numbers for a programming kata

you want the tests to be random?
you could generate ~10 tests, hardcode them in, and not expose them to the user

#### Kenny Lau (May 15 2020 at 22:14):

that is impossible, as demonstrated by the back-and-forth in https://leanprover.zulipchat.com/#narrow/stream/238266-Codewars/topic/hackproofing.20programming.20katas

#### Jalex Stark (May 15 2020 at 22:17):

oof

Last updated: May 17 2021 at 15:13 UTC