Earlier quoted context omitted.
> This is very neat. Cheers! > Do you have anything similar for Prolog? Well, what you think of "Formal Methods: A First Introduction using Prolog to specify Programming Language Semantics"? https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf Abstract > An important fundamental idea in formal methods is that programs are mathematical objects one can reason about. Here we introduce students and developers to thes…
Oh, that paper is very interesting, thanks for that. It's not really comparable to a fully formal system, though: The user essentially chooses which trivial things to prove to convince themselves of something. For example, a real proof assistant would tell you what exactly to prove for the inductive proof in the factorial example. In this system you pick an induction principle yourself and hope it's correct. Still, I…
There's also PRESS, which seems relevant, "Solving symbolic equations with PRESS"
> We describe a program, PRESS, (PRolog Equation Solving System) for solving symbolic, transcendental, non-differential equations in one or more variables. PRESS solves autonomously, i.e. without guidance from the user. The methods used for solving equations are described, together with the service facilities. The principal technique, meta-level inference, appears to be relevant to the broader field of symbolic and algebraic manipulation.
https://www.sciencedirect.com/science/article/pii/S074771718...
https://github.com/maths/press
I'm not trying to promote Prolog over TLA+ or anything, I've only just started with TLA+.