The official tutorial's interactive features are broken.

[kindaro]

As far as I could ascertain, the official tutorial is located at https://ucsd-progsys.github.io/intro-refinement-types/120/. It has little «play» buttons in the upper right corner of interactive snippets, such as the one in subsection Exercise: Positive Integers. Pressing this button results in an error message showing up that says: Request failed0.

The cause of the error seems to be that some additional content is being fetched by HTTP, but it is not allowed on modern browsers to fetch stuff by HTTP from a page that was itself fetched by HTTPS, because it is not secure.