cubicaltt VS plt

- cubicialtt a programming language based on cubical type theory in which univalence from homotopy type theory isn't an axiom but a theorem

If you’re interested in programming languages specifically, the current state of the art is called Cubical Type Theory. CuTT has lots of flavours and the community hasn’t coalesced around a single design. The paper I personally found easiest to digest was the “ABCFHL” paper, but I’d recommend reading it alongside the original CCHM paper. None of the publications made an ounce of sense to me until after I’d digested Favonia’s YouTube channel, Mortberg’s lecture notes and this other series of lectures from Harper (particularly the final one).

I updated the blog post to include some people in academia who contributed. I've been interacting with Kent Palmer and Sylvester James Gates, Jr. The latter held lectures about the philosophy of mathematics. I've been using work inspired by Vladimir Voevodsky, e.g. cubicaltt (https://github.com/mortberg/cubicaltt), which is also performed by academics.

I recall reading a comment on here at some point in the last year where someone who worked on a team that wrote compilers lamented the difficulty in hiring qualified people because the practice of compiler construction differs so wildly from what is taught in school or even most compiler books. Apparently it scarcely resembles what is taught in university courses based on the Dragon book or similar, both in the higher level architecture and the lower level techniques

I know that one difference is that compilers have adopted a more service-oriented architecture, kind of like the Roslyn compiler. This allows them to not only compile your code, but inform your text editor and linter and similar tooling of syntax issues incrementally.

What are other differences? Is llvm still relevant outside of academia?

Are there any books, papers, or open source projects one could study to learn how compilers are built in this day and age?

Also: does the more abstract "programming language theory" popular in the more formal functional programming world (e.g. denotational semantics, lambda calculus, Floyd-Hoare logic, type theory, etc: this sort of stuff[1]) have any relevance to compiler writers and language/language tooling developers in industry?

[1] https://steshaw.org/plt/

Programming Language Theory books and resources

steshaw/plt - A path to Programming Language Theory enlightenment