uwm-masters-thesis VS theta-idl

Neat! This proposal caused me a lot of headaches, mechanizing its specification was the primary contribution of my Master's thesis a couple years ago[1]. Glad to see it finally moving forward after stalling for so long! Excellent work!

[1]: https://github.com/jacobmischka/uwm-masters-thesis/releases/...

I've found it comes up pretty often. Sometimes because the logic I'm writing demands it—traversing over some kind of nested recursive structure, for example—but more often because it makes the code easier to read. A real-world example: I have a little interface description language which can generate code in a few different target languages. I want to factor out some of the more complex logic (eg dealing with record types) into self-contained, testable functions, which means that my top-level toDefinition function needs to call toRecord, which needs to call toDefinition for each of the record's fields[1].

(Sorry if it's hard to follow the code without context, but that's the problem with examples—either they're too trivial to be interesting, or they're complex enough to be a bit confusing!)

Additionally—and maybe even more importantly—tail call elimination also makes code written in continuation-passing style (CPS) more efficient. While CPS isn't something we usually want to write by hand, a lot of common abstractions (async libraries, promises, monads) map to CPS under the hood.

[1]: https://github.com/target/theta-idl/blob/stage/theta/src/The...