Recursive functions are possible in a total system as long as the recursion depth is bounded. The original Boyer-Moore theorem prover (1978) had that. You had to prove termination for every recursive function by giving a depth value, which could be a function of the inputs. For example,
(times x y)
(if (zerop x) 0 (add (y (times (sub1 x) y))
There's a lot to be said for working with total functions and finite arithmetic. No undecidability, no halting problem.
He mentioned Sentient Lang in the article. It is really, really cool. Its a compile-to-JS declarative logic language that can do some fucking neat stuff. Think Prolog or Mercury, but with much more comprehensible syntax.
I reached out to him a month or two ago after stumbling upon his work, and he took the time to respond and have a conversation with me.
Incredibly brilliant and genuine guy, happy to see more of his stuff posted here.
Edit: He has done more stuff besides Sentient. Check out his work in the general area of computational logic/automated theorem proving.
Regarding the following considerations:
"After a few seconds this program terminates which seems wrong. Why should a problem that has infinitely many solutions ever terminate? Shouldn’t it run forever?"
Yes, conceptually, it should of course run forever. However, at some point, even when using unbounded integers (which it, in my view, also should do), it will eventually run out of memory because the representations of involved bounds will exceed what can be stored.
In such cases, from a correctness perspective, it is inadmissible to simply stop "silently", because that would be indistinguishable from cases in which there are no (further) solutions.
Instead, some kind of error should be raised, indicating that it was not possible to search further than that. And when using bounded integers, likewise an error should be raised if some internal range is exceeded when searching for solutions.
For eg if I’m designing something in the real world I’d want to optimize for material or cost in terms of time or money.
Sometimes I’m just interested in seeing if a solution exists.
So the solution here seems to be able to add soft constraints on what kinds of solutions are desired to guide the search.