Charlag is a user on birb.site. You can follow them or interact with them if you have an account anywhere in the fediverse.
It's #Coq time again and once again I will not be able to prove that eval actually terminates becase it uses auxillary (nontrivial) function which I cannot inline and I don't want to make another hack.
Y'all think Haskell is so robust with its purity?
Only when you write in something strict you understand how much it is optimized for ergonomics and not for correctness.
Partial functions, unbounded recursion etc break mental model. You can (and should) stay away from them as much as possible and use good subset.
Also Haskell has tons and tons of info these days (relatively ofc). Not at all with Coq which is super old but still lacking a lot of info.
