Post #1721541

After @mflatt's discussion on call-by-need yesterday, I'm thinking about GHC internals again. I'm back to my side quest of formalizing a small language that was written in Haskell, as implemented, including all the bugs from unintended laziness. Revisiting the STG machine papers now after ~4 years, they're much more approachable. I'm thinking I'll model STG in Rocq or maybe Lean, hack GHC to dump my STG for the language, then model an optimized version of the language without space leaks and as much of the GHC substrate simplified as possible, and prove equivalence. Wow, that's a lot. Reading time! #programminglanguages