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.


If you like my work, please consider buying me a coffee.


overview