Samizdat reviews and mentions

• The semantics of a simple functional language
  1 project | news.ycombinator.com | 12 Mar 2023

  where "eval _" in Lean becomes "ev x", and "_.embed" becomes "ve _".

  The theorem body is heavily commented (nice!), and each case is handled explicitly and in full. While the development is probably a little bit longer than in Lean or Isabelle, I find it easier to approach.

  [1] https://github.com/pigworker/Samizdat/blob/main/ExampleSeman...

  > I could not write this stuff. It looks simple but it isn't.

  True that. I bounced a number of times off of proof assistants before it stuck. Like I said, I feel very comfortable with Agda now; but I won't claim this is easy.