Nice paper on an interesting topic. I’ve not had a chance to read the paper thoroughly, but the judgmental equality ended up weaker than I anticipated. I’d hope we’d end up with alpha-equivalent codefs being judgmentally equal.

Which makes me wonder what the next steps for a proof assistant based on this is. Will the de-/refunctionalization play an active role in the proof assistant as well, thus solving it as described in section 4.1?

I assume you refer to his results regarding axiomatic systems for arithmetic on natural numbers? If a law attempts to capture this, then, sure, it's problematic. But I don't that's very common.

From what I've seen, formal methods for legal systems would take the "facts" of a case as given (assumptions), and deduce legal consequences of those.

I'm using what is probably the simplest static site generator: cat.

  for f in texts/*.html; do
    cat preamble.html "$f" postamble.html > out/$(basename "$f")
  done

The front-page is written manually.

I did something along those lines once, but I used https://github.com/susam/mdme as the preamble so I could write the posts in markdown rather than html. The index was an extra line to add links to index.html.