It doesn’t always happen like that, where the big difficult thing you just learned becomes trivial. I’ve observed that for some people, learning something really difficult, getting over the barrier of incomprehension and suddenly mastering the concept, can produce a feeling of satori, like a strong spiritual experience. It’s happened to me a couple of times. Finally figuring out how ShaderToy programs work, by reading the source code for numerous shadertoys (hint: signed distance functions and sphere tracing). Another was learning Haskell and finally “getting” the idea of pure functional programming. For other people I’ve talked to, it has been other programming languages. Then, for some, this can lead to a religious conversion, a feeling of religious zeal for your now favourite programming language, and proselytization.
I never even thought of doing the 5 with outside throws. For me, 6 balls is where it gets into wizard-level (or genetic freaks if I’m being kind to myself). Though it’s been years since last I even saw my bag of 6-panel Dubé’s. Unlike with programming and math stuff, I feel like getting to the next level in juggling just required exponentially more effort.
Anyway, what made me really realize the amount of blub I’ve picked up was trying to explain how one would code an app in practice to my kid. There’s just soo many layers and pieces of arcana and bureaucracy involved, it made me wish for an alternative world designed by Xerox PARC or something.
I feel like for me the next spectral line in formal methods is “learn what the hell De Bruijn indices are”. I keep running into them on the implementation side of formal methods (used inside Z3 & the TLA+ proof checker) and they really seem like the bedrock of everything else.
Probably it’s the same in juggling, but I think for the things you mentioned in formal methods & distributed systems it is just a matter of investing the time to learn. Sure there’s some floundering at the start because it’s often impossible past undergrad to find introductions to a concept at the exact level that’s right for you, but all the things on your list could be accomplished with 1-2 months of dedicated full-time study for each. I don’t think skill ceilings would really apply.
Oh yeah, that’s the other thing. It’s like Herculean to learn this stuff if you have a real job. If anybody reading this weekend-warriored their way to this knowledge then count me as deeply impressed.
One of the classic problems when implementing the lambda calculus is name capturing. There’s a nice description on p.21 of Simon Peyton Jones’s book. The classic solution is alpha conversion, i.e., renaming variables so that they don’t collide.
De Bruijn indices avoid the need for alpha conversion by eliminating variable names. Instead, each use of a variable is replaced by a reference to the lambda that binds it.
Usually (especially on paper) these references are represented by counting the number of nested lambdas between the use of the variable and its binding site, e.g.,
λx.x → λ0
λx.λy.x → λλ1
Beta reduction with de Bruijn indices is trivial with normal-order leftmost-outermost reduction, because the arguments are closed terms. But if you are simplifying inside a lambda term, an argument can have free variables referring to an enclosing lambda, which look like a de Bruin index larger than the nesting depth of the argument. These free variables will need their indexes adjusted when they are beta-substituted into a lambda body.
It doesn’t always happen like that, where the big difficult thing you just learned becomes trivial. I’ve observed that for some people, learning something really difficult, getting over the barrier of incomprehension and suddenly mastering the concept, can produce a feeling of satori, like a strong spiritual experience. It’s happened to me a couple of times. Finally figuring out how ShaderToy programs work, by reading the source code for numerous shadertoys (hint: signed distance functions and sphere tracing). Another was learning Haskell and finally “getting” the idea of pure functional programming. For other people I’ve talked to, it has been other programming languages. Then, for some, this can lead to a religious conversion, a feeling of religious zeal for your now favourite programming language, and proselytization.
I never even thought of doing the 5 with outside throws. For me, 6 balls is where it gets into wizard-level (or genetic freaks if I’m being kind to myself). Though it’s been years since last I even saw my bag of 6-panel Dubé’s. Unlike with programming and math stuff, I feel like getting to the next level in juggling just required exponentially more effort.
Anyway, what made me really realize the amount of blub I’ve picked up was trying to explain how one would code an app in practice to my kid. There’s just soo many layers and pieces of arcana and bureaucracy involved, it made me wish for an alternative world designed by Xerox PARC or something.
I feel like for me the next spectral line in formal methods is “learn what the hell De Bruijn indices are”. I keep running into them on the implementation side of formal methods (used inside Z3 & the TLA+ proof checker) and they really seem like the bedrock of everything else.
Probably it’s the same in juggling, but I think for the things you mentioned in formal methods & distributed systems it is just a matter of investing the time to learn. Sure there’s some floundering at the start because it’s often impossible past undergrad to find introductions to a concept at the exact level that’s right for you, but all the things on your list could be accomplished with 1-2 months of dedicated full-time study for each. I don’t think skill ceilings would really apply.
Oh yeah, that’s the other thing. It’s like Herculean to learn this stuff if you have a real job. If anybody reading this weekend-warriored their way to this knowledge then count me as deeply impressed.
De Bruijn indices are neat!
One of the classic problems when implementing the lambda calculus is name capturing. There’s a nice description on p.21 of Simon Peyton Jones’s book. The classic solution is alpha conversion, i.e., renaming variables so that they don’t collide.
De Bruijn indices avoid the need for alpha conversion by eliminating variable names. Instead, each use of a variable is replaced by a reference to the lambda that binds it.
Usually (especially on paper) these references are represented by counting the number of nested lambdas between the use of the variable and its binding site, e.g.,
Beta reduction with de Bruijn indices is trivial with normal-order leftmost-outermost reduction, because the arguments are closed terms. But if you are simplifying inside a lambda term, an argument can have free variables referring to an enclosing lambda, which look like a de Bruin index larger than the nesting depth of the argument. These free variables will need their indexes adjusted when they are beta-substituted into a lambda body.
Unfortunately I was never exposed to Lambda calculus as an undergrad so that’s something I’ll have to learn beforehand.