Sure but we will no longer be able to benefit from the first-rate work
done by PlusCal as regards states and transitions modelization.
In fact I like PlusCal. If we consider TLA+ is a universal machine like Turing machine
(I only use the words in an unformal way), PlusCal shows what a procedural
language is. It just shows what "procedurality" is. And, I would say, in a
very pedagogical way.
Maybe somebody would like to do the same thing for a functional language, a mock-lisp,
just as Plus-Cal is a mock-C. A pure functional language obviously.
It would be called Plus-Func, for instance.