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.

The concatenative and functional language F:

http://www.nsl.com/k/f/f.htm

How do you define success in terms of your work?

Chuck: An elegant solution.
One doesn’t write programs in Forth. Forth is the program. One adds words to construct a vocabulary that addresses the problem. It is obvious when the right words have been defined, for then you can interactively solve whatever aspect of the problem is relevant.
For example, I might define words that describe a circuit. I’ll want to add that circuit to a chip, display the layout, verify the design rules, run a simulation. The words that do these things form the application. If they are well chosen and provide a compact, efficient toolset, then I’ve been successful.

https://www.oreilly.com/library/view/masterminds-of-programming/9780596801670/ch04.html