Philip Wadler

It does sound like you might be after something closer to totality checking. I'm not as familiar with that, but I can maybe give a few pointers and a bit of terminology:

One easy way to guarantee termination, even for functions with input/output spaces that are infinite, is using "structural recursion". This is when we only make recursive calls on a 'smaller piece' of our input. The classic example is the `Natural` type, where we can do:

f Zero = somethingNonRecursive
f (Succ n) = somethingInvolving (f n)

We can tell just from the syntax that the argument will always get smaller and smaller for each recursive call. Note that structural recursion is syntactic: we cannot do something like `f n = f (n - 1)` since the syntactic form `n - 1` is not a 'smaller piece' of the syntactic form `n`; whereas `x` is a smaller piece of `Succ x`. This makes structural recursion pretty limited. As an example, the "Gallina" language of the Coq language/proof assistant does totality checking via structural recursion, and it very quickly becomes unusable (more on Coq below!).

There's actually a subtlety here: if `Natural` is defined inductively then all of its values are finite (it is the least fixed point of its constructors, sometimes written as a "μ" or "mu" operator; similar to the Y combinator). In particular its values are `Zero`, `Succ Zero`, `Succ (Succ Zero)`, and so on. This means that structural recursion on `Natural` will eventually stop, either by hitting `Zero` or…

You might like to try out Mandelbrot Maps. It allows real-time interactive exploration of the relationship between the Mandelbrot set and associated Julia sets. (There is a corresponding Julia set for each point on the Mandelbrot set, and some striking structural similarities.) Also, the images it produces are beautiful. :-)

Disclaimer: I wrote the original version for my MSc project 7 years ago. Future students added further improvements in later years, including notably creating two Android apps. All versions are free and open source software.

- https://play.google.com/store/apps/details?id=uk.ac.ed.inf.mandelbrotmaps - Android app port, by Alasdair Corbett

- https://play.google.com/store/apps/details?id=io.bunnies.fractalmaps - Updated Android app (Fractal Maps), by Sky Welch

- http://homepages.inf.ed.ac.uk/wadler/mandelbrot-maps/ - Original Mandelbrot Maps (Java applet), by me

- Wadler's blog: http://wadler.blogspot.co.uk/2015/04/fractal-maps.html | http://wadler.blogspot.co.uk/2012/03/mandelbrot-and-julia-surprising.html | http://wadler.blogspot.co.uk/2008/09/mandelbrot-maps.html

This piece is intended as an accessible intro; it talks about the beginnings of formal logic, how intuitionism in the debate on foundations of mathematics led to intuitionistic logic, and Gentzen's natural deduction.

It seems the only other HN discussion about a post on natural deduction so far was this one: https://news.ycombinator.com/item?id=22324836

There is also one on Curry Howard:
https://news.ycombinator.com/item?id=17748717

It's from there that I found "Howard on Curry Howard", a published response to a letter Phil Wadler wrote to William A. Howard. It provides an excellent hint how Martin-Löf's work on dependent types was influenced by the Curry-Howard correspondence and natural deduction.
https://wadler.blogspot.com/2014/08/howard-on-curry-howard.html

>I also dispute the claim that a strong type system is a "tiny factor" in code quality.

There actually are some studies that show that using a static typing system is only a tiny factor when it comes to code quality:

http://wadler.blogspot.co.uk/2011/09/experiment-about-static-and-dynamic.html

However, I've also read studies that show the opposite, but the lack of rigurosity and the possible confounds that show up for both sides seems to render this as an open question.

Consider that fact that prime-minister of Singapore knows Haskell by now

http://wadler.blogspot.com/2015/04/prime-minister-of-singapore-plans-to.html

He is already quite good with C++

https://arstechnica.com/information-technology/2015/05/prime-minister-of-singapore-shares-his-c-code-for-sudoku-solver/