Zulip Chat Archive

Stream: Is there code for X?

Topic: random number generator


view this post on Zulip 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

view this post on Zulip Chris Hughes (May 15 2020 at 21:27):

I remember seeing one somewhere in core I think.

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 15 2020 at 21:27):

but it doesn't use the system time

view this post on Zulip Reid Barton (May 15 2020 at 21:27):

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

view this post on Zulip Kenny Lau (May 15 2020 at 21:30):

how do you read a file?

view this post on Zulip Chris Hughes (May 15 2020 at 21:31):

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

view this post on Zulip Kenny Lau (May 15 2020 at 21:32):

I just want random numbers for a programming kata

view this post on Zulip Reid Barton (May 15 2020 at 21:36):

like this: https://github.com/leanprover-community/lean/blob/master/leanpkg/leanpkg/manifest.lean#L105

view this post on Zulip Kevin Buzzard (May 15 2020 at 21:37):

Kenny Lau said:

I just want random numbers for a programming kata

I would recommend 37

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jalex Stark (May 15 2020 at 22:17):

oof


Last updated: May 17 2021 at 15:13 UTC