It seems increasingly obvious that the expectation for the return on the capital invested into AI is “the ability to run a complex economy without needing to pay lip service to the pesky moral scruples of the intellectual and engineering classes”, a true wet dream for capitalists who can now turn into full extraction mode without needing to worry about alienating the smart people.

In an unparalleled triumph for “cycle on train” ideology, I have arrived at the Cambridge computer laboratory 3.5 hours after getting out of bed in Wolfson College, Oxford.

We have the terms computer scientists and computer engineers; why not add the terms computer logicians and computer mathematicians to the mix?

I do think that computer mathematicians and computer logicians are somewhat different from a computer scientist. For instance, @shriramk is a true computer scientist; he experimentally derives new empirical facts about computing. The type theory community has historically mostly consisted of computer logicians and computer scientists, but for instance HoTT, SOGATs, synthetic Tait computability, brings type theory into computer mathematics. Domain theory is of course an early instance of computer mathematics as well.

(I somewhat prejudicedly associate “computer logician” with tedious syntactical proofs and “computer mathematician” with semantic proofs.)

Do people have recommendations for socialist/anarchist journals/newspapers/online magazines to follow? I'd be especially interested in any that have long-form articles which are not just about current events.

Even worse, the error I was getting was fixed by importing a module...

While I am happy that Haskell has `x.a` syntax for accessing record fields, it is incredibly frustrating that it uses unification instead of synthesizing a type, because the error for `x.a` being the wrong type is the same as the error for `x` not having field `.a`...

Some thoughts on document formats. https://owenlynch.org/blog/hypertext-documents/

If you are working on a software project with me and you use Claude, I won't complain or stop you, I'll instead judge you and shit-talk you behind your back.

And you should expect a significant fraction of your coworkers to do the same; could be anyone.

And then instead of 30 minute talks, each day starts with 4 lightning talks and then the rest of the day is reading the source code for the presented languages.

I want a PL conference where the only allowed submissions are new programming languages and the acceptance criteria is coolness.

In Italian, almost every word ends with a vowel. Is there any language where every word starts with a vowel?

In violin playing, there's a term "violinistic" to describe music which works well mechanically with respect to how the bow and fingers naturally want to play things. Moreover, different keys will bring out different resonances: the Bach G-minor sonata first movement would hit differently if the first chord didn't have two open strings, for instance.

I want to use "type theoretic" in a similar way to describe constructions that both work well mechanically with Coquand's algorithm and come naturally with a decent categorical semantics. It's a similar feeling; once you have worked with SOGATs and have implemented nbe a couple times, you start to get a sense which constructions are "type theoretic" and which are ad-hoc syntactic b.s.

But "type theoretic" works less clearly as an adjective than "violinistic", where it is clear that this is a made up word that you then should ask the definition of. @pigworker wrote "bidirexual" recently, which captures some of this.

Rule 1 of decent-performance software: don't prematurely optimize, only optimize after benchmarking.
Rule 2 of decent-performance software: don't benchmark prematurely, only benchmark after a real-world use of your software is slow.
Rule 3 of decent-performance software: use first-principles thinking so that your software never ends up being slow in real-world use 🙃.

It's always a bit shocking to me how intellectually unserious our not-so-benevolent corporate overlords are.

https://paulgraham.com/earn.html

Paul Graham, the so-called "great essayist" has given a speech about earning a billion dollars which amounts to "it's very possible to earn a billion dollars if you grow your company very fast, dur dur leftists don't understand compound interest" with absolutely no engagement as to the substance of the objection, which is about what "earning" ought to mean. Namely, even taking at face value the dubious claim that startups are "creating wealth" rather than simply figuring out ways to create existing services in a way that avoids regulation and then pocketing the savings from not having to obey the law, does the owner have a morally legitimate claim to that wealth over the workers?

But PG seems completely unaware that there's even an argument to make here?

I suppose it's not prudent to wish one's enemies were smarter, but like, come on.

Someone needs to start a grant program for algebraic geometry and call it the fellowship of the ring.

The old fashioned way of doing language design which had a standard and multiple implementations had some downsides, but I do kind of miss design for reimplementability because it's a good forcing function for some kind of simplicity...

Something similar could be said for green threads/actor models but I'm not as familiar with these.

I really feel like generational garbage collection is underappreciated, and not enough part of people's mental models when they compare GC languages to manual/Rust-style memory languages.

In a GC language, "heap objects" are *much cheaper* than "heap objects" in a language with manual memory management, because they are first allocated on what is essentially a bump allocator, and then if they survive long enough, are allocated as part of a *bulk* allocation.

Casey Muratori talks about "n+1 programming" which is when you shift from thinking about individual objects in your program to collections of objects. A well-tuned runtime system for a GC language is *precisely* this; it handles memory management in batch-mode. https://www.youtube.com/watch?v=xt1KNDmOYqA

In order to recover the performance of a GC language doing tree manipulation in a manually managed language, you have to completely rearchitect your code to think in batches, use custom allocators, etc. Which is possible, it just means that the idea of "writing functional-style code in Rust" is a lie. You have to work at a fundamentally lower level of abstraction.

A runtime system is *not* just some cope that managed languages need in order to run, it's a tool that you actually may have to reimplement when you don't have it.

The responses to this prove that humans rock :)

I'm trying to stick to my "ask mastodon rather than chatgpt" habit: does anyone have recommendations for interesting places to visit in Paris?