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.

• 1: Hello triangle, first thoughts
• 2: Some animation
• 3: Preliminary performance test
• 4: Troubles with linearity
• 5: Linearity continued
• 6: Bye IO monad, hello GL monad
• 7: Short code quality update
• 8: Baby’s first dependent type
• 9: Ensuring uniforms belong to bound program
• 10: Implicit arguments & monad transformers
• 11: No linearity with monadic errors (for now)
• 12: Linear algebra with linear types… not great
• 13: Slow and frustrating progress
• 14: Getting back into it
• 15: Restricting arguments to a list
• 16: Binding programs again
• 17: A Hoare state failure
• 18: Hiatus