4 ms·
"I don't think type theory has a whole lot to do with programming or software engineering. The most practical languages ... do not have sound type systems" wel
by dustingetz 15y ago
"I don't think type theory has a whole lot to do with programming or software engineering. The most practical languages ... do not have sound type systems"
well i mean most software isn't understood, using Linus's metaphor, most software works due to "years and years of testing on thousands of machines", not due to "thinking and analyzing"[1]. and, i think, teams that are capable of "think and analyse" can out-compete teams that don't.[2]
[1] http://www.dustingetz.com/linus-think-and-analyze-motherfucker http://www.dustingetz.com/linus-think-and-analyze-motherfuck...
[2] http://www.dustingetz.com/re-seth-godin-how-do-you-know-when-its-done http://www.dustingetz.com/re-seth-godin-how-do-you-know-when...
- barrkel 15y agoI think this more relates to mindfulness as you work through a programming problem. I know that when I am very tired, I can sometimes succumb to the "random walk" approach to debugging, where my reasoning takes a rest and I start coming up with theories as to why the program isn't working, and start changing little things to see if they fix it. If it was graphical work, it might be changing + to -; if it was one of my current bugs right at this minute (relating to dynamic linking on OS X), it would be adding an extra indirection to a pointer lookup. This "approach" is sometimes faster than the mindful "think and analyse" way, but only by chance, and only when your approach was roughly correct to begin with. And I agree that the "think and analyse" technique is better; rest is usually better than the random poking, which can also introduce a bug that bites you a few weeks later. But "thinking and analyzing" I think also applies to my problem with type theorists! They spend a lot of time coming up with new ways to use various formalisms to capture various intents of the programmer (like the deadlocks and accounting of effects in an uncle post), but they don't spend much time doing science: the kind of science that happens when you have a control group. They've got their heads down at too low a level. That's a bit of an attack on the whole edifice of computer "science", but I think it's long overdue. I don't think we're going to find any magic formalism that revolutionizes the world, making writing programs of arbitrary complexity trivial for schoolchildren. I think we need to spend more time looking at actual people, their strengths and weaknesses, and crafting our formalisms around those - and that work is only honest if it actually measures effects on average joes doing work, not rework of existing programs by talented graduate students.