Making WebGL typesafe in Idris 2

I’d wanted to learn Idris for a while, and see how far I could realistically take type-safety. In particular, can I ensure all documentation of the WebGL spec is encompassed in types? (thus achieving correctness-by-construction).

The writing is not particularly well curated. This a log of my thoughts while learning and developing. Views and opinions will change throughout the chapters. I will probably be wrong often.