Thinking about a random number generator

[konnov]

If you liked or disliked the blog post, leave a comment, upvote this discussion, add a star to the repo

[josef-widder]

I like the explanation of the thought process.

I have a comment which is not really of the center of the text. The sentence "Hence, we can informally rewrite Property (2) as follows:" that introduces Property 2' is a bit handwavy as it glosses over probability distributions and potential loops in the state machine etc. But again, this is not super important ;-)

[konnov]

It is hand-wavy. Probabilities are hard. That's why I wanted to get rid of them as quick as possible :)

[0xekez]

I really liked this blog post! Thanks for writing it. The inversion of property two in the second part is neat and something I hadn't thought of before.

[0xekez]

Do you have any suggestions for exercises or things I might try and model/verify in quint? I'd like to practice these skills, but don't know how to find practice projects.