I spent a not-insignificant amount of time learning how to do proofs with Isabelle. I learned a lot about inductive proofs, set theory, meta-logic, and challenged myself to prove a lot of the stuff I had previous taken for granted (e.g. proving that different sorts refine each other). I enjoyed it, and similarly was convinced that this was going to be some life-changing thing that changes my career trajectory and...
Nothing changed. No one in charge of companies gives a shit about theory. They all claim that they love theory, they claim that they are very research focused, they claim that they value all the time you spent learning this stuff, but in reality they really just want you to change the color of buttons, or change the format of dates, or add a field to a JSON. It sometimes feels like no software engineer but me actually wants to learn any math, and will refuse to touch anything even resembling it.
And I'm not picking on Isabelle here; I've had similar results trying to pitch TLA+ and Coq and Agda for some of the more error-prone parts of the codebase, with different sales-pitches, and without fail the managers will always say that they "will look into it", and promptly do absolutely nothing. The first two times a manager said that, I believed them, but after that I realized that they're just trying to shut me up and tell me "no" politely.
It was enough to depress me, and it still kind of does.
I still think learning stuff for fun is worth it, but I'd be lying if I told you if I knew why.
If you work on webshit like me you won’t get to use these skills much.
(On the other hand, recursing over the structure of JSON-like data often feels like 80% of the job, so I think the skills come into play at least a tiny bit).
I don't get to recurse over JSON, occasionally I get to design a system from scratch and that's more fun, but it's usually not more complicated than "draw boxes that point to other boxes and/or cylinders on screen". Sometimes I draw a picture of cloud.
I like my job just fine, it's a decent job, and I like my managers and coworkers as well, but it's just disappointing that enthusiasm for math and theory is what got me to this stage of my career, but I never really got to use it, and I don't see that ever really changing for me.
Maybe I will write a paper at some point at least.
I made the mistake of telling an employer, and whenever I made any mistake in my work, no matter how small, the employer would immediately say that the PhD work is distracting me, and my focus not BigCo.
My PhD is on an indefinite hiatus right now, because it’s something I am questioning the utility of right now.
I can definitely see a lot of utility depending on what you do research in. I bet a lot of ML doctoretes are making big bucks, but that's relatively niche.
ML is cool but I was never able to get super into it. I use ChatGPT but I never had a ton of desire to get into the guts of it. I was always more interested in discrete math and formal logic.
Im in the same boat. I like abstract logic/math and ML never caught much of my interest.
I want to start applying but Im not even sure how to find departments that would fit what Im looking for. Maybe I need to take this more seriously and start reading papers and self study.
Recursion? Oh you mean proof by induction?
Cryptography? Oh you mean number theory?
Neural networks? Oh you mean calculus?
Almost everything I learn while programming can be associated with some theory I learnt before for math.
I don't know anything about neural networks yet (though I really need to get on that), but I have noticed the other two examples you mentioned as well; recursion is more or less applied inductive proofs, a lot of crypto boils to number theory.
My dream is to some day convince a manager to give me budget to spend a few weeks designing a new system and proving correctness with TLA+. I'm not saying it's terribly likely, but a man can dream.
Compare with all the moaning and complaining that comes from some people when you talk about functional programming and how it might relate to computer science.[1] Then you might have a better chance inventing ad hoc words for basics like “map” (preferably very prosey) and claiming that Martin Fowler invented it.
[1] This goes triply for anything having to do with proofs, at least proof software associated with FP.
It is easy to tell if a tennis instructor is giving “good” instruction, where good means instructions that help you be a better tennis player. You just look at their students. If you want to know if they give good fundamentals for long term growth, you look at their much older students.
How do you know if a meditation teacher is giving good instructions? Seems much harder to me.
It is interesting that many of the traditional religions have hard to quantify benefits. Buddhism offers a personal inward help, and the abrahamic religions often benefit communities.
But schools typically teach these things as a "theory part" and as "practice/application part" (for example by "syncing/sequencing" courses if possible) which helps with both relevance and "getting it".
And it’s not just terminological: the difference becomes very important when you realise one needs to prove that recursion is possible (that is, function definitions by recursion on a well-ordered set are well-defined) by induction. So one actually comes logically before the other.
I guess to truly determine whether they’re distinct concepts you’d have to exhibit some model of set theory that supports recursion but not induction, or something. But that’s beyond me.
IIRC Church was heavily influenced by Turing and vice versa.
Being on the engineering side of things without much knowledge/focus on programming languages theory and the mathematical nature of computation, one feels as if all the niceties we have in popular PLs are just laws of nature that we just had to discover, whereas in reality they too had to be derived, tried, improved first. But then you study something like this and expect to be able to finally connect the dots and yet, it's still not immediately obvious how we arrived here!