🚀 go-pugleaf

In article <3570@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes:
>Until now, I have argued the necessity of
>the denotational-semantics-based approach
>for higher-order functional programming.
>Now me say a word for the opposition.
o

This seems like an opportune time to put in a plug for the Primitive
Recursive arithmetic [1]. 
While this formal method has received little attention in the c.s.
community, it has numerous advantages over more widely known methods.
In particular, p.r.a. has an algorithmic notion of function that seems
better suited to the world of c.s. than the set theoretic notions
implicit in predicate calc and denotational semantics.  
Also p.r.a. allows for a completely formal approach, i.e. functions as 
textual objects, without requiring clumsy axiomatizations of ordinary
arithmetic. The proof rules are simple substitution rules for equality
e.g.  A = B |- F(A) = F(B) , and the axioms are the defining axioms of
the p.r. functions. 


1. Goodstein "Recursive Number Theory" (Noth Holland 1957)