Do not worry I understand 99% of your message. It's indeed a land far far away from the everyday coding of the majority of programmers. Unless they start digging, which I did. If you take code as data (lisp roots showing) you start to want to reason about it and quickly you end up reading about FP, denotations, different forms of evaluations, the value of metadata (type or else).

Now I believe there's an artificial split between math leaning people and pragmatics, the former end up as PhD, the latter in IT or close. But in reality the average coder could understand and even enjoy the land of abstractions, it's just that the river he swims in isn't flowing there so one has to run against the flow.

Not to say that ideals are the only-tru-way.

I am delighted you responded so positively to what I wrote and didn't take what I wrote negatively which you could easily have done.

Let's for arguments sake say that there are two camps (broadly speaking), the pragmatists as you say and the theorists/idealists let's call them. It reminds me of the difference between someone like Torvalds and someone like Stallman.

Thing is we need both! You're right, the split _is_ artificial. The Linux kernel couldn't wait for someone to come along and create a type-awesome version of C. I mean, Rust seems to be the first attempt to take what type theorists have learned and apply it to a systems programming language. In the meantime software needs to be written and we have the tools we have.

If the fruits of type theory are going to filter through into software development I'm not sure it should come laden down with category theory (as awesome as that is) or the lambda calculus (as mind-bending as that is). I could of course be dead wrong.

A guy tried to make a C-level formal language, even sexp based at first. After years he quit, saying it's probably impossible to have both (he wrote a long long article about the reasons, he didn't leave without explaining every problems in details).

Usually ideas filters in tiny bits, kind like genes. See closures, forever in lisp, but now in every languages while lisp is still niche.

The issue with theorists is that they see the world in abstract algebra / combinatorics, it's not fluff, it's just extremely high level thinking with extremely short notation[1]. It looks like straight BS until you spend enough time seeing that it translates into reality. Say something like prolog, where a few rules give you graph coloring. It's not theory only, it's actual application of different semantics.

[1] also, as in any group, they developped a culture and taste for some things, expressing everything in the form of arithmetic expressions. F^n <= iteration of F n times, it's a loop in average coder lingo.

This was fantastically well stated.

Type theorists are people who understand arrows very well -- as long as those arrows aren't pointers. :)

ba-dum tss! are you here all week?

Sure---if catering keeps that sirloin roast coming for another seven days. Have you tried it?