Raymond Smullyan, To Mock a Mockingbird (1985)

Charles H. Moore, Programming a Problem-Oriented Language (1970)

This is extremely intriguing to me not because it is employing my old love Lisp and new love Forth, but also because it has been surrounded by my new rabbit hole in type theory that I've been exploring, gradual type theory and the work of Paul Levy. So call-by-push-value is one of the brilliant ideas that I've come across recently. And his Forsp is exactly this.

In fact, while reading about CBPV, I couldn't help but think "That's Just Forth!", and thus Forsp was born.

void push(obj_t *obj)
{
  state->stack = make_pair(obj, state->stack);
}

bool try_pop(obj_t **_out)
{
  if (!state->stack) {
    return false;
  }

  *_out = car(state->stack);
  state->stack = cdr(state->stack);
  return true;
}

This is just something I never thought of being done. You have a stack operation which is implementing car and cdr.

Fun little fact: You can use simp? to extract the list of lemmas that simp applied.