Thank you! I’ve tried to make sure that my site reads well and loads fast, even on mobile.
There’s actually no JS on my site at load time, I run it all as a build step that transforms Markdown with inline LaTeX into pure HTML and CSS. https://github.com/azdavis/azdavis.net
No comments on the writing, but one thing to add: the syntax highlights for code get lost a bit. I would see them better either if they were a lighter black (aka dark grey), or had a different background than the rest of the text.
Do you mean the inline code or code blocks? In any case, I tweaked the background to be more different from the page background (in both light and dark mode) and also gave inline code that same background. Does that help?
https://github.com/azdavis/azdavis.net/commit/55199593abfb6e...
Nothing to add to the other comments, just wanted to add another data point that the website (on mobile) was perfectly clear and the information was all laid out and explained very well; I have no (constructive) criticism to give.
Great post! I was going to share this one on the r/functionalprogramming subreddit when I found yours. A lot easier to read, and helps reading the Wikiversity afterwards. Thanks!
The definition I gave at the end of the article (the thing starting with `t ::=`) is basically a context-free grammar describing the syntax for terms of the calculus of constructions.
`t ::= ...` is saying "A CoC term, called t, can have the following forms ..." Then each case is separated by `|`.
The cases for application, abstraction, and forall are recursive, in that they contain t (or t') when the thing being defined is also called t. (The prime on t' is just to say that t and t' can be different terms.)
So for instance, the case for application is:
t(t')
That means if you already have two arbitrary CoC terms, called t and t', then if you write down first the term t, then a `(`, then the term t', then a `)`, then you've written down another CoC term representing the application of the term t to the term t'.
And the case for abstraction is
λ(x:t) t'
That means if you have two CoC terms t and t', then if you write down `λ`, then `(`, then a variable name (x is kind of a meta-variable-placeholder name, you can name the variable whatever you want), then `:`, then the term t, then `)`, then the term t', then you've written down an abstraction term. In this case, the variable x (or whatever you called it) has type t, and can appear free in t'.