Kategorienpest @maxsnew@types.pl

The usual syntax for regular expressions is not a regular language because it requires parentheses. The usual syntax for context free grammars/expressions is not context-free because it uses recursion using variable names.

Is there any fundamental reason for this, i.e., some kind of diagonalization/fixed point argument or is it just a coincidence? I think the Goedelian argument doesn't apply because they are weaker than Peano arithmetic?

CBV and CBN as syntax sugar for a CBPV core language?

Everyone else has imposter syndrome but I am the one person who actually is just lucky/a fraud.

Hard-core Curry-style/extrinsic typing advocate gives checks for unbalanced parentheses at runtime

Doing advent of code with a toy/young language:

Expectation: Time to implement some cool data structures!
Reality: Time to write lexers/parsers! (Either by hand or implement some parsing libraries)

Eating some dogfood, probably a bit prematurely tbh (https://github.com/maxsnew/aoc-zydeco)

This is from the classic "Lambda: The Ultimate GOTO" paper. Sad that this is only taken seriously in functional languages to this day and we have new platforms like WASM that don't take advantage of this lesson.

Also, this is exactly how CBPV works.
1. `GOTO` is in CPBV `force`ing a thunk,
2. Pushing a return address onto the stack corresponds to the "bind" `x <- M; N` construct. You push the kont `x. N` onto the stack.

We have hardly anything implemented so it ended up looking like assembly code but here's day 1 solution in our CBPV language Zydeco: https://gist.github.com/maxsnew/d0e3f47bd136aa5b3d17c906d00b38d9

Probably won't be able to keep this up very long since we haven't implemented parameterized datatypes, polymorphism or even imports yet but it was fun to get the very easy one working.

Close to finishing my first compilers course where I actually teach parsing/front-end in some depth. While I think there is usually over emphasis of particular algorithms over general principles, I was struck by the fact that the front-end is treated much more systematically and mathematically than the backend: different front end passes (lexing/parsing/type checking) are given mathematical specifications in terms of grammars/declarative type systems and then we need an algorithm to implement the spec.

Compare the backend where specs are usually very informal and so correctness is fuzzier. It's a bit funny bc most of my research is on semantics that only applies to the backend. But perhaps that's exactly why we emphasize mathematical specification of the front-end more: because it's already been figured out while the backend is research or at least involves more PL semantics than we can fit without a prereq.

Anyway at least this gave me the idea to give my last lecture on compiler correctness and verification and to frame it in these terms.

Regular Expressions : Logic Programming :: DFA : Functional Programming ?

Very bizarre that Rust's test lib supports Result<T, String> as an output type but then doesn't display that string in the error message if the test fails. Should probably just use some unit testing crate that provides a better interface.

Ugh after the utter schlock that has been coming out of Disney Star Wars for years now finally they make a good show (Andor)? I'm so skeptical but everyone is saying it's so great...

In the spirit of "teaching category theory in the context of applications" my category theory course for next semester is somewhat morphing into an axiomatic + denotational semantics course.

There's a special place in hell for people who design a new target for language implementation that doesn't support tail calls/goto...get ur act together WASM