lambdaxymox

F# always struck me as one of the most terribly underrated languages. I'm a lover of MLs in general, but F# lands on one of the sweet spots in PL space with ample expressive power without being prone to floating off into abstraction orbit ("pragmatic functional" is the term I believe). It is basically feature complete to boot.

I don't know about superoptimization, but JetBrains does have a HoTT-based language and proof assistant called Arend for doing mathematics in.

For sure among the hardest problems in software engineering are versioning dependencies, and managing dependencies. At least those are the two I find the most aggravating. It seems like almost nobody can get it right even though component-based software engineering, SoA, etc. I think are generally extremely good ideas. The execution is pretty crummy pretty much everywhere.

With all that said, my sense is that hardware engineering has its own heap of Sisyphean problems and complexities. I definitely would not go back to working on hardware engineering problems like I did super early in my career (a mix of embedded firmware, device drivers, PCB design, and web development). I shudder at the thought of ever working with anything Verilog/VHDL, Xilinx, or SPICE ever again, or debugging PCB designs on the bench top in the lab with an oscilloscope and a logic probe. At least in school I ran more than a few bodge wires to patch a mistake in a PCB design iteration. Maybe in some sense, it's a blessing that those linear systems theory abstractions fall apart utterly in RF engineering problems, and one has to contend with the fact that all circuits radiate. At least circuits that still contain the magic smoke.

Maybe I'm different, but I used Kleinberg/Tardos and CLRS in my undergraduate algorithms class, and I preferred CLRS to KT and the other alternatives (Algorithm Design Manual, etc.), though KT was great too. I've heard from others that KT was better for them for learning how to actually design algorithms as well.

Interesting, I must have lucked out quite often and got the first printing back in the mid to late 2000s since back then virtually all of my print Springer books I bought back then were sewn-bound.

The construction of MIR titles reminds me a lot of older Springer GTM and Grundlehren der Mathematischen Wissenschaften series titles. I have a number of Springer titles I've picked up over the years and the older printings were beautifully typeset and bound with very good paper. I try to find the older printings of Springer books when I can when chasing down a copy for my personal library.

I find coffee products to be a frustrating product category. At least for me, I have adverse reactions to certain blends of coffees--particularly nausea, coldness, and headaches--while other ones don't cause trouble at all, so I have to try different coffee blends with a bit of caution. I notice that any amount of coffee past the second cup in the morning doesn't really add anything to my alertness, productivity, or ability to pretend to be a morning person--with the bulk of the benefit being from the first cup--but anything past the second cup makes it harder to fall asleep later at night. I can only imagine how one gets so far as to put down a pot of coffee a day (and then some!) for years on end.

Jean Yves-Girard's thinking evolved from analytic philosophy to continental philosophy over the course of his life, and in this book in particular, some of his asides and polemics critique how we conceptualize truth, knowledge, and logic, and how other fields conceptualize that stuff, from a continental perspective. The fact that this kind of stuff turned up in a mathematical logic book of all places really struck me. It put me on a path to taking a more serious interest in the continental school, and reading more of it (currently chewing on Gilles Deleuze and Bruno Latour). It's a very unusual and difficult book, that led me to very different (compared to what I am used to, anyway) modes of thinking.

The Blind Spot: Lectures On Logic by Jean Yves-Girard

For context, Girard is a mathematical logician, philosopher, and co-discoverer of the type system System F (Haskell, ML, etc.). The book is a monograph on proof theory, and I was interested in learning more about affine and linear logic to deepen my understanding of Rust and other language ecosystems focused around the ability to explicitly model resources. However, along the way, I learned some other great things: (1) continental philosophy is deep and cool; (2) mathematical writing can be simultaneously rigorous, clear, and hilarious; and it reinforced (alongside Alain Connes's Noncommutative Geometry, and various French philosophers) (3) French academic writing is both frustratingly and delightfully idiosyncratic. Girard writes polemically about other aspects of knowledge, mathematics, etc., and there's heaps of dry humor and anecdotes throughout the book. It's a hard book to read even by pure mathematics standards--a topic not exactly known for being a brisk read--but it was worth it just for the side discoveries alone.

I discerned a similar ontology as the OP over the years in different hobbies too. My sense is that what quadrant one leans into can change in time and space too. In my case, I've had a whole heap of nerd hobbies in my life, among them being game collecting and retrogaming.

I was a game collector even when I was a child back in the heyday of console generations 4 and 5 all the way into my mid twenties, and also a game player since then up to the present as well. When I was much younger I used to love collecting original hardware and media complete in box and everything, and I kept everything I got when it was new in absolutely pristine condition (I was a very atypical child) but as I got older I grew tired of the collecting aspect of video games and sold everything off. At some point it dawned on me I was just buying stuff and putting it in a box (falling into the kit quadrant) and not really playing the games at all. After realizing all that, and when I had acquired everything I wanted (I tended to collect a mix of only games I liked + genre instead of by system, so my collecting requirements were much smaller and easier to achieve), the fun was over and I cashed out some years later. With retrogaming I now vastly prefer a Raspberry Pi and a gamepad in the living room. Fortunately I was able to get in and get out of the game collecting hobby when it was a fairly cheap hobby to participate in (i.e. when CIB copies of classic games were like tens of dollars at most).

I was also an avid tabletop gamer who was into the playing and collecting aspect of Magic: The Gathering and other TCGs, particularly Legend of the Five Rings, Vampire: The Eternal Struggle, and VS System. I started playing MTG way back in the ancient days and had a particular taste for vintage. I also played standard, booster draft, legacy, and extended, but vintage was always my favorite. Back then vintage was accessible on a high school budget with planning and dedication, and wasn't the rich man's game it now, at least if one is not using proxies. For a long time I was both into the competitive side of the game, as well as the collecting side of the game. Over time I grew tired of the playing aspect of Magic: The Gathering and vastly preferred the collecting aspect of it, before life priorities changed entirely and I lost interest in TCGs completely.

I don't really do the collecting/kit hounding side of any hobbies anymore, I prefer the actual doing of the thing instead, but I am grateful I was able to get in, enjoy it fully, and get out of the collecting aspect of both video games and MTG long before both became impossibly expensive to participate in, though it is fun to dip in and see what is going on with those things from time to time.

Not stated in the article, but I suspect that another big reason a lot of hobbyists obsess over the gear and kit aspect of a hobby is because buying kit is a substitute for not having time or energy to actually do the hobby itself. In some sense, buying kit is materializing fantasies about actually doing the thing, but not having the time or the place to do it.

Type inference occasionally bites one's hand when pushing data across an FFI boundary. In one instance I was writing some graphics code for a project and for some reason the colors in the rendering model were coming out all wrong on the screen (TL;DR it ended up looking like two of the color channels were missing from some texture maps) and it turns out that Rust inferred the type of the buffer as a vector of f64s instead of a vector of f32s. Putting the type in specifically fixed the problem promptly.

Lesson learned: Sometimes type inference fails, and always annotate your types at FFI boundaries!

I know two people who worked through SICP. One of them had so much fun with it they worked through it twice cover to cover in their free time. In both cases they reported to me that SICP was quite a revelation to them, since Scheme is about as simple a practical programming language as one can get other than maybe stack languages like Forth. That is, while [un-|simply-]typed lambda calculus and Turing machines are simpler models of computation, I wouldn't exactly call them practical models of computation. In one case they said that it really gave them real purchase on what computation really means. That is, what is it really about when one strips off all the type theory, build tools, and dependency hell. My sense is that SICP is better left to after getting a couple years of experience doing computer programming to appreciate though for most people though.

Are the enterprise versions of Windows 11 also filled with bloat?

I got some keys second-hand for Windows 10 Enterprise LTSC a few years ago, installed it on some ten year old hardware at the time, and I was honestly surprised how responsive Windows could be absent (to the best of my knowledge) the telemetry software, Cortana, etc., and how fast it could boot. It's almost like the true blue good Windows experience without all the nonsense is secretly reserved for only business customers and pirates.

Some problems are good problems to have. If different groups of people are taking the time to substantively and constructively complain about different shortcomings of Rust and its ecosystem, it shows that there's a wide enough audience of serious users out there. My take is that the Rust devs are doing something right, even if it seems like they can't win.

One of the great parts about linear algebra is that there is almost always a simple geometric idea underneath.

The geometric picture underneath is one of the things that keeps me in awe of the subject despite its seeming simplicity, and I keep getting something out of it every time I come back to it. It's a bummer since finite-dimensional linear algebra is one of a handful of mathematics topics where one can answer all the questions posed at the beginning of a course in it by the end of a course in it, so it is a pretty self-contained topic.

After learning e.g. exterior algebra (differential forms), Clifford algebra (geometric algebra in these parts), and so on, the geometric picture of the determinant as the size of an oriented volume makes deriving the algebraic formula super duper slick. Like in Clifford algebra, the formula can be proven in two or three lines. It's unfortunate that it seems like e.g. exterior algebra never get introduced sooner in the pedagogy of linear algebra or multivariable calculus because when used right they make the underlying ideas shine through beautifully. It's a bummer since exterior algebra is much simpler than it looks, though like many things in mathematics, it's takes a lot of work to make that simple idea rigorous. But unfortunately algebra in general given it's abstract nature can absolutely lobotomize the real deal geometric ideas underneath a lot of this stuff when used poorly.