This is one of those essays that I’m happy to have read and upvote but I take a lot of issue with where the author’s going.
Oddly enough, my problem is that he fails to realize that Computer Science, like every other academic discipline and organizational silo, becomes self-reinforcing and less useful the more you stay inside one lane. You can pick any lane, Category Theory, Type Theory, and so on … and then do one of these surveys of the good, the bad, and the ugly about them. At the end, I’m not sure there’s any “there” there.
Writing applications bridges theory and application, with application coming first and theory following along behind. That’s true whether we’re writing applications in Finance or talking about our own disciplines. Make it work, get something useful out of it, then learn a little more around the periphery to make sure you didn’t miss anything. But for the love of the Great Pumpkin, don’t pick up any one of these silos and do a deep dive trying to find some golden morsel of wisdom about programming you wouldn’t find otherwise. It’s not there. Or rather, there’s so much there, and it’s so detailed, that sorting the useful from the bullshit (and both of those from the simple distractions and ad-hoc pointless arguments) that there’s no value there.
Put another way, the value pulls the useful from the theory. This is why the best way to learn a new programming language is to take what you’re learning and apply it to a personal project. At some point you’ re going to realize that all of those new STL tweaks in C++ don’t mean squat to you and maybe never will. That doesn’t make them useless for everybody. It’s just a recognition that you’ll probably never be looking for value where they might be useful. Then you’ll start looking around and seeing that kind of thing everywhere. It’s a personal decision and there’s no right and wrong to it. It’s all about value.
So while I love survey essays, and I think if nothing else they’re great for sorting out your thoughts, I part ways once we start talking about universal attributes of things being useful overall or not. It doesn’t work like that.
Thanks for the work, though! There’s a ton of useful knowledge in the work you’ve done. You obviously know your stuff! Looking forward to reading more from you.
I’ve picked up reading Types and Programming Languages after having read the Structure and Interpretation of Computer Programs in college followed by the Essential of Programming Languages. Having spent nearly 9 years as a software developer, I can’t say any of it has been useful. I’d have probably done better to interest myself more in the business problems at hand than to expend energy reading through these books that are too academic for most programmers. What’s more, I’m pretty certain that I’ve met other programmers who are blissfully unaware of recursive data types, regular expressions, or anything else that programmers could pride themselves on knowing but they’re better than me at getting code working, simply and without fuss. Maybe because they’re better problem solvers or maybe because their view of programming hasn’t been crowded out with theory.
But what keeps me going, or what I tell myself, is that the occasional opportunity does come up in which this exposure to theory results in some direct or amusing application. It does happen and then I feel that my time hasn’t been wasted. Could also just be intellectual wankery on my part though.
Well, I don’t think it’s wasted if your aim is to learn to build languages – as Steve Yegge says, everyone should learn to build a compiler. However for people who want to jump into it I would recommend the OWASP cheatsheets – which are far more relevant to programming practices than most of this fluff.
What kind of applications do you develop? I’ve certainly used a little bit of theory here and there, and where I did have to use it I probably wouldn’t have been able to get the job done at all (or in any reasonable amount of time or with reasonable results). But not even needing regular expressions, that sounds to me like a very strange situation.
Maybe you’re simply doing work for which you’re overqualified?
Haven’t seen you in a while. I’ve been out of tech for unusual, life-changing reasons (see profile). Glad you’re still trying to help people become better programmers. I noticed a few things where I might be able to help. It was some disagreements where I’ll just give some examples you might think on and work with your own way.
I’ve seen all kinds of good stuff happen in practice with types. It’s easier for people to learn about. There’s a range of formality. The sheer amount of innovation that gets real-world results makes me strongly encourage all kinds of people to explore type theory, systems, and techniques.
There’s a series of lessons from program analysis that can be summed up as “design your programs to be easy to analyze.” I’ll add for humans as well as machines. Good structure, specs at interfaces (eg contracts), hierarchical calling with limited loops where possible, limiting side effects, and even using previously-analyzed libraries can all help. Then, you benefit from current tooling. Easy-to-analyze code will often benefit from other tooling down the line. Then, use a mix of tools that are each good at different things.
The other thing I’ll note is building the tools. There’s not going to be a magic analyzer. What there can be is a combo of specs and software that are fed into multiple analyzers that all use their own formats, techniques, etc to output useful results. For example, lets say you automatically tranform a non-distributed app into represenations used by SV-COMP tools, concurrency checkers, and info-flow tools like SIF/JIF. After that, guided or fuzzed testing using top, free tools w/ specs in there as runtime checks. That will catch a lot of problems.
I’ll also note findings like Microsoft’s claim memory safety was 80% of their real-world vulnerabilities and Linux fuzzing catching tons of problems. By the numbers, building a diverse array of program analyzers seems to be one of highest-ROI investments that researchers can make. Qualifier: they must be easy to build/use, free, and open.
I occasionally brainstorm this for fun. I don’t know it has any use. Exception are DSL’s for things like state machines, data sharing across networks, configuration, maybe optimizing data structures, etc. I saw good results for SIMD synthesis recently. Computers can already do this kind of thing better than humans if the humans are non-experts or time-constrained.
That reliability/quality is low importance to both industrial and FOSS developers means this is probably not important at all. If it’s done, I encourage the automated tools to be used for exploring designs (eg TLA+, Alloy), proving properties of higher-level forms via automated provers, and proving lower-level properties (eg SPARK Ada). I encourage this for the high-value components of software where it doesn’t burden development. Far as manual verification, I’d only encourage that at this point for components of the automated, verification tools I just named. As in, annotated or push-button tooling for as much as possible with it hand-verified for its own trustworthiness until they’re good enough to verify themselves automatically. Note again, though, that I’ve narrowed the Who in this paragraph several times until we’re not talking about mainstream programmers. You and I are in this target audience, though, so I thought I’d share my recent “automated methods just for key stuff mainstream can use.” Think miTLS, not “X in Coq or Isabelle.”
I still don’t know anything about this. Like most stuff, I default that all the progress we’ve made in software engineering without it suggests we don’t need it. I won’t deny it might be useful at some point. The database example you cited is the kind of stuff I like to see. Then, I have to ask empirical stuff of those people like, “Does it handle common failures in file systems? Does it have efficiency of non-C.T. implementations? Does it do concurrency safely? And is it just as elegant or better when it does all three?” Again, I’ve done no research on it to determine the answer to such questions.
Just some observations in case you found any interesting or helpful.