I found sokuza-kanren [0] to be a wonderful introduction. It starts with the absolute basics and builds into a minimal logic system through a series of well-documented steps.
> loops like this are easy for compilers to analyze, in a way that makes them not representative of real code
Which makes it a perfectly fine benchmark to measure whether a particular compiler implements these optimisations. The benchmark also highlights fine implementation details. I did not know about Dart's interrupt checks, for instance.
I see these microbenchmarks as genuinely useful, as I can analyse them, the logic behind them, and apply results in interpreter design. Consider [0] for example. Any sane compiler would do this kind of optimisation, but I've seen only one production interpreter (daScript) doing it.
[0] https://github.com/miniKanren/sokuza-kanren