sigil

Great essay, thanks for sharing.

When I was a software library developer, I came to resent application developers. I noticed a pattern. Libraries solved hard problems and did so carefully, thoughtfully, in a way that others could reuse. Apps would come along and carelessly, recklessly glue together several high quality libraries into a piece of software targeting a general audience. The apps would then harvest all the credit.

What's happening in mathematics right now feels similar. Applications (theorems) were always how one built objective reputation, but libraries (concepts, definitions, boring lemmas) were also rewarded socially within the mathematics community. And individual mathematicians often managed to both build their own libraries, and use them to prove an important result. And then those libraries were sometimes of use in other results.

Bessis asks whether AI Lean proofs will land in Mathlib or Mathslop. Or in my framing: will they be libraries, or applications?

At present they're mostly Mathslop. The proven result is perhaps useful, but the methods employed aren't novel or reusable. I worry that this trend will only worsen, because applications make headlines, and the libraries they used do not. We are not properly incentivizing library development in OSS, or in math, or in infrastructure writ large. There's a serious credit assignment problem here.

What might change this? Once the low hanging fruit is picked, will citation count rise in relative status again? Will we get result fatigue and start to reward legibility — no one cares unless the paper has an accompanying ELI5 tiktok video? A labeling regime that certifies the proof was produced sustainably, organically, by local artisans with no AI additives?

"Every augmentation is also an amputation." – McLuhan

https://driverlesscrocodile.com/technology/neal-stephenson-o...

There's a reason Spotify might force shuffle play on the free tier. It isn't solely to annoy you into upgrading. Royalties are 2x - 5x higher for interactive vs non-interactive streaming plays.

Are human rights concerns running cover for more straightforward financial interests here? Norway and Saudi Arabia are both petrostates with large sovereign wealth funds.

> I believe the bounding box has to fit all the possible ascenders and descenders etc., so the em-height is proportioned within the box to whatever the highest and lowest marks in the typeface are.

I wish it were this simple.

The em square != the bounding box of all glyphs. The em square is defined by the font's ascent & descent vertical metrics, which are set by the font designer.

There are reasons why you might want glyphs to escape the em square. Perhaps you're typesetting English text without accent marks above capitals, and using the bounding box's vertical maximum would introduce too much line space. Or perhaps you're using a decorative font which is designed to escape the em square, and potentially even overlap the em squares of lines above and below, like this: https://alangrow.com/images/blog/script-font-escaping-em-squ...

To make matters worse, and mostly for legacy reasons, there are THREE different sets of ascent & descent metrics in a font file. Which is used depends on your OS and the software rendering the font. But the Webfont Strategy described here is a nice one, because you can use the bounding box (winAscent & winDescent) if you really need to, say because any glyph might be used and you want to avoid em square escape: https://glyphsapp.com/learn/vertical-metrics

nginx validates hostnames per the spec, and to your question specifically it rejects requests that would put a slash in $host: https://github.com/nginx/nginx/blob/b6e7eb0f5792d7a52d2675ee...

This nginx local dev config snippet is one-and-done:

  # Proxy to a backend server based on the hostname.
  if (-d vhosts/$host) {
    proxy_pass http://unix:vhosts/$host/server.sock;
    break;
  }

Your local dev servers must listen on a unix domain socket, and you must drop a symlink to them at eg /var/lib/nginx/vhosts/inclouds.localhost/server.sock.

Not a single command, and you still have to add hostname resolution. But you don't have to programmatically edit config files or restart the proxy to stand up a new dev server!

These are neat. I'm reminded of Claude Mellan's face of Christ from 1649. This also uses a single continuous line, but he was carving the line by hand into steel!

https://www.gallery.ca/magazine/your-collection/a-familiar-f...

Gleick's "Chaos" got me sent to the principal's office in high school. I went crazy for fractals. Unfortunately all I had at home was an IBM PC XT. Mandelbrot set renderings were agonizingly slow and the CGA palette was too limiting.

Around this time my co-conspirator and I realized the library had 386s that almost no one was using for catalog search. They became our fractal render farm. We'd exit the catalog program, insert a floppy with our latest renderer, kick off a deep zoom, and turn off the monitors to avoid suspicion until we could check back next period. The results were thrilling. What a difference the access to compute made.

You all know the story -- eventually the librarian found us out and reported us for "hacking."

Thank you!

Who was the first person to propose FFTs for faster polynomial multiplication?

Got curious about this recently. I’m not great at citation tracing, but did make it back to this 1995 paper by David Eppstein [0] where he uses it to efficiently solve Subset Sum after an incremental update. Surely Knuth’s TAOCP had it even earlier?

The fact that FFT polynomial multiplication also lets you solve Exact Subset Sum with Repetition in sub-exponential time came as a real shock to me. [1] Crucially, this algo is O(N log N) where N = the maximum element, not N = the set size, so it isn’t a P ≠ NP counterexample or anything.

[0] https://escholarship.org/content/qt6sd695gn/qt6sd695gn.pdf

[1] https://x.com/festivitymn/status/1788362552998580473?s=46&t=...

> Sure, but how often do you need to touch that config?

More often than I’d like! tmux config has broken backwards compatibility on me multiple times over the years.

This is fine for most software — you upgrade your config once and you’re done. However, the nature of tmux is that I use it on many servers, some old and some new, some with tmux 1.x and some with 2.x. Getting a ~/.tmux.conf from my dotfiles repo that works across both has been papercutty.

Love tmux though & can’t imagine tty life without it — I run it locally as well as on remote machines.

> And on a related note, Lewis Mumford, a philosopher and writer, wrote quite a bit about how clocks were (in his view) the necessary invention for capitalism to flourish.

Szabo also takes this up in his excellent essay "A Measure of Sacrifice":

Fair broadcast and verification of time was thus of fundamental importance to the most common contractual relationship in the new European cities. In agricultural societies, including medieval Europe, serfdom and slavery had provided most of the labor. Most workers in a modern economy earn wages based on a time rate. Along with or following the rise of the time-rate institution – including the contracts themselves, the laws and regulations governing the contracts, and the technology to fairly measure the principal quantity – came the growth of related economic institutions, such as the joint stock company. These institutions enabled a boom in productivity and the spectacular rise of Europe from its darkest ages to the modern era. We will now chart the rise of the clocks and the institutions they supported.

https://www.fon.hum.uva.nl/rob/Courses/InformationInSpeech/C...

HTML can be described by a context-free grammar [0], but not by a regular grammar [1]. If a language can be described by a regular grammar, you can parse it with a regular expression -- that's where the "regular" in RegExp comes from!

Derivatives of RegExps don't automatically unlock parsing of context-free grammars, afaik. For that you need recursion. They do however unlock some very elegant parser designs.

[0] https://en.wikipedia.org/wiki/Context-free_grammar

[1] https://en.wikipedia.org/wiki/Regular_grammar

This idea was used to great effect in Matt Might’s “Parsing with Derivatives” paper [0]! And it featured prominently in the Compilers class he taught at the University of Utah.

[0] https://matt.might.net/papers/might2011derivatives.pdf

Lol okay man. Maybe if you're running FreeBSD 4.2 or HP-UX or some BSD derivative from the 90s. All unix systems from about 2000 on will honor unix domain socket permissions.

Like you, we use pre-signed S3 upload urls. From there we use Transloadit [0] to crop and sanitize and convert and generate thumbnails. Transloadit is basically ImageMagick-as-a-Service. Running ImageMagick yourself on a huge variety of untrusted user input would be terrifying.

[0] https://transloadit.com/

You do realize D-Bus also uses SO_PEERCRED right? And transitively polkit, systemd, and everything in that ecosystem.

https://gitlab.freedesktop.org/dbus/dbus/-/blob/master/dbus/...

> Meaning you have to be incredibly careful what you do when creating the socket and you cannot really pass any sockets off to other processes if you want to try to do security that way because they will still inherit the wrong credentials.

I see nothing new here beyond "handle privileged resources with care." Don't overshare. Got an open pipe to `sh` running as root? Maybe you oughtta set O_CLOEXEC on that fd before you exec and overshare with a child. Got a socket that's been peer authed? The same.

This is pretty basic unix stuff. If you stick to the basics and avoid the siren call of complexity, the security properties remain relatively easy to reason about. Most privileged resources are fds. Mind your fds.

I'm not a huge fan of sending file descriptors over sockets – maybe we agree on that part.

What do you mean by "great ideas and great implementation / bad execution and bad interface." Is this a plumbing vs porcelain distinction?

I like s6! One of the key differences here is that s6-sudo builds on, rather than replaces, the standard unix permissions model.

s6-sudod listens on a unix domain socket. Unix domain sockets are just files, so they have an owner, group and mode bits. The answer to "who is potentially allowed to run a differently-privileged command?" is just `ls -l /path/to.sock`.

For finer-grained access control, a unix domain socket listener can call `getpeereuid()` or `getsockopt(..., SO_PEERCRED, ...)` to learn who it's talking to. You can build powerful – but still relatively simple, and importantly, readily-inspectable – access control policy on top of these basic unix primitives. That's what s6 does. Look at how simple rule definition is. [0]

Or, you could throw all that out the window and build something much more complex and much less inspectable, which is the systemd approach. The answer to "who is potentially allowed to run a differently-privileged command?" under `run0` is to...spend the evening reading through polkit xml rules, I guess?

I realize systemd uses D-Bus, and D-Bus uses a unix domain socket. But that socket is writable by world. We're trusting polkit and complex policy xml and probably a constellation of other services to get things right after the SO_PEERCRED check.

Maybe that's fine for desktop apps, but a reminder that we're talking about sudo here.

Complexity is the enemy of security. The complexity of the systemd ecosystem broadly writ is how we get CVEs like this polkit privesc, which took 12 years to notice [1].

Addendum: it's possible to regard systemd as dangerously complex AND sudo as dangerously complex. OpenBSD as usual had the right idea with `doas`.

[0] https://skarnet.org/software/s6/s6-accessrules-cdb-from-fs.h...

[1] https://www.cvedetails.com/cve/CVE-2021-4034/

run0 has already been exploited: https://twitter.com/hackerfantastic/status/17854955875146385...

There will be plenty more where that came from. Yet another terrible idea and terrible implementation from Poettering.

Paper: https://arxiv.org/pdf/2404.03095.pdf

Good question! Here's a paper, "Build systems à la carte: Theory and practice," that compares Make, Shake, Bazel, and Excel:

https://ndmitchell.com/downloads/paper-build_systems_a_la_ca...

Yes, Excel can be considered a build system! A cell outputs the result of a computation, but it can also input computation results from other cells. For performance reasons, you don't want to recompute all cells in a spreadsheet when one cell changes. You want to do the minimum – an incremental rebuild. You do that by traversing a DAG with cells as vertices. You might not be "compiling" "files", but it sure looks like a build system in other important ways.

I've worked on build systems on & off for most of my career, but your question made me realize I've never read a book that presents build systems in the abstract. Everything I know comes from studying specific build systems and, in some cases, writing my own. The design space for build systems is huge and still expanding. That makes a unified theory of build systems difficult.

Can you share what motivated your question and what you're hoping to learn?

The accompanying code lets you try this [0].

  make -B DICT=/usr/share/dict/british-english
  ...
  ca,co,de,di,ed,er,es,in,li,mp,ng,nt,ra,re,ri,si,st,te,ti,ve

No "ph", but definitely a different optimal tileset! British English swaps "mp" in for "ar".

[0] https://github.com/acg/lettergen/