> invoking incompleteness is like invoking Russell’s paradox — important for foundations, but often a distraction in practice
Yes, but the operative word here is "often". "Often a distraction" is logically equivalent to "sometimes relevant". The problem is that whether or not it is relevant to you depends on your goals, and different people have different goals. For example, one of my goals is pedagogy, and so it's really handy for me to be able to fire up a CL REPL and do this:
Clozure Common Lisp Version 1.12.1 (v1.12.1-10-gca107b94) DarwinX8664
? (expt (sqrt -1) (sqrt -1))
#C(0.20787957 0.0)
> The intrinsic (Church) view builds meaning into the syntax itself.
This is what I don't get. I can't even wring any coherent meaning out of the phrase "build meaning into the syntax itself". Programs don't have meaning, they are descriptions of processes. Programs don't mean things, they do things.
Even for natural language sentences, which do mean things, I don't understand what it could possibly mean to build meaning into the syntax. "The dog ate my license plate" has meaning but "The dog ate my car crash" does not despite the fact that those two sentences are syntactically identical.
(BTW, imbuing syntax with meaning sounds more like Chomsky than Church to me. But what do I know?)
> I’m most comfortable rejecting “correct” code.
Again, one of my goals is pedagogy. Towards that goal I once wrote this:
https://flownet.com/ron/lambda-calculus.html
After writing that, I thought this might be a good time to learn Haskell. If CL is good for showing off the lambda calculus surely Haskell will be even better? I'm guessing I don't need to explain to you why that did not go to plan.
And BTW, thanks for the kind words.