undefined | Better HN

0 pointsigravious8y ago0 comments

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.

0 comments

agumonkey8y ago

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.

jcranberry8y ago

This was fantastically well stated.