RE: https://abyssdomain.expert/@filippo/117472790782832037

Yes, very much this:

"We have proof automation now": https://www.imperialviolet.org/2026/07/26/zstd-lean.html

In which someone who's terrible at using interactive theorem provers wonders whether dependently-typed languages might be interesting now that the machines can easily write the proofs for you. Also there's zstd involved.

Since custom little utilities are now almost free for the technically-minded, I guess I value of ideas for them has increased.

In light of that, two things that have been making my life slightly better this week:

* A Chrome extension that lets you select any div on a page and then downloads the contents of that div (including images) as an EPUB for putting on an ereader.

* A job that runs on a little server that monitors my email and, based on a YAML file of regexps for sender, subject, etc, will notify me via Pushover if a matching email is received. (No polling, thanks to JMAP.)

It seems that py/cryptography's thoughts about OpenSSL (https://cryptography.io/en/latest/statements/state-of-openssl/) are doing the rounds at the moment.

I've not touched OpenSSL directly in a long time. In fact, it appears that the 10-year anniversary of that (https://www.imperialviolet.org/2015/10/17/boringssl.html) passed by a few months ago!

So I've no direct comments on the piece but, a long time ago, I was in the position where I was landing changes in both OpenSSL and NSS (Mozilla's TLS library). OpenSSL was somewhat famous for having bad code. And, indeed, if you looked at it back then the functions were full of single-letter variable names with pointer arithmetic everywhere and context-free, somewhat scary comments. It wasn't outside the norm for 1990s C code, but I understand why people recoiled.

In contrast, if you looked at NSS code, it looked good! Consistent formatting (before clang-format), good naming, good comments.

But NSS had a PKCS#11 abstraction layer and, even after years, I never could understand how the control flow worked there. I would have to single-step in gdb every time to figure out where an operation grounded out into actual code. I was reminded of that when reading py/cryptography's descriptions of OpenSSL 3.0.

I had a pet theory at the time that, because OpenSSL was repulsive on the surface, it inhibited people enough that they couldn't add much deeper complexity. But NSS, with its invitingly clean-looking code, was understandable and then people had enough capacity left over to add deeper complexity.

There might be something to it, although you shouldn't discount the fact that entities who are willing to fund cryptography libraries often have demands that are contrary to clean code. Things like FIPS compliance and compatibility with a zoo of different accelerators and bespoke needs.

So rather it might have been that old OpenSSL was old OpenSSL because it was mostly unfunded. That meant that it looked pretty ragged, but also there weren't so many demands in tension with good design.

NSS was funded by interests that really cared about PKCS#11 compatibility so that you could use a super-expensive, certified-everything HSM with it. When OpenSSL got shocked into switching to a higher-funding model, that brought lots of those same sorts of competing interests, and then the incentives pointed towards adding slow, impenetrable layers of abstraction all over.

Even when the underlying reality changes, the status quo has a strong grip. People are deeply creatures of habit. It's also difficult for the emerging understanding to overcome the barrier of becoming "common knowledge" and, prior to that, people will follow old patterns because they assume that it's expected.

High-salience events create new common knowledge and so lead to larger changes in behaviour than might otherwise be justified. For example, the '56 Suez crisis was a high-salience event that communicated that world power had shifted from Europe to the US. Its impact was much greater than a narrow analysis would convey.

The Russo-Ukrainian war and today's events are also high-salience, and they communicate that there aren't any rules any longer.

One consequence is that, in the absence of Pax(ish) Americana, the only effective defense is a nuclear one. This was well understood: a lot of the motivation for creating the post-WWII system was to create an alternative to nuclear weapons. But Libya gave up its program and Gaddafi ended up dead. Ukraine gave up its weapons and got invaded. Venezuela didn't have them.

It'll take a while for this to play out, but I suspect keeping it in mind will help with understanding the news over the next decade or so.

How come James Cameron is the only person who can make 3D movies?

There were trailers before it, in 3D, and they looked bad. But then Avatar itself is visually stunning — again. ("IMAX" 3D.)

The first Avatar was revelatory but audiences (including me) quickly learnt that in every other case 2D movies were actually better than than the 3D version.

Except Avatar movies, which continue to be astonishingly pretty. This one is even better looking than the last due to mostly avoiding the weird frame rate switches.

If you find yourself traveling, cooking, cleaning, etc by yourself in the coming week, one of my favourite podcasts has had a great series on tracking down some nasty bugs recently.

Consider it like a murder mystery podcast, but for systems issues. If that sounds fun to you, peruse:

https://oxide-and-friends.transistor.fm/episodes/futurelock

https://oxide-and-friends.transistor.fm/episodes/grown-up-zfs-data-corruption-bug

https://oxide-and-friends.transistor.fm/episodes/death-by-uptime

For whoever needs to hear this: Your monitor should turn on promptly when the machine wakes up.

It turns out that my monitor cable has been slowly getting worse over years and, because the degradation was so gradual, I became insensitive to it. It would take five or more seconds for my monitor to switch on after waking my machine. Occasionally it wouldn't manage to come on at all and I would have to press the key combo to lock the screen and then wake it again.

Finally it got to the point where the monitor would sometimes go black for a few seconds and I replaced the cable. Now I'm surprised every time it responds promptly.

In "UI continues to be hard" news:

Heading from Manhattan to JFK Airport, I got on an E train because you can take that to Jamaica Station and then get the monorail to the airport. But once I was on the train, I noticed that it was going to Jamaica 179th Street. But that is not near Jamaica Station. If you look on a subway map, an E train cannot go to Jamaica 179th Street, but I've lived in New York for years so this doesn't faze me. I hopped off the train, caught the E train behind it, and that was going where the map said it should.

But as a visitor, how on earth are you supposed to know that this train is ignoring the map and going to a station called Jamaica that is not the Jamaica Station that the map says it goes to?

When you get to the correct station, there are signs for the airport; great. But if you follow them, you get dumped out onto a Queens street corner. If you turn 180 degrees you can see the LIRR station, but there are no airport signs anywhere. I've done this lots of times so I know that the monorail is attached to the side of the LIRR station. But, again, how on earth is a visitor supposed to know this?

Lastly, while boarding the plane, rather than an agent with a barcode scanner there were two automated gates with barcode scanners. One lady was getting frustrated because she was trying her phone as if this was an NFC interaction. So, yea, in a payments context you use your phone like that, but in a boarding-a-flight context you have to flip it over and press the screen against the glass. I guess people are supposed to figure this out based on whether there's a barcode on the screen.

Then I wondered whether she was distracted because she had to fight her way to the airport from 179th Street because the subway can't follow its own map.

You need to read over the bulk of the (pretty good) documentation before using, but I think https://www.nushell.sh/ is worth trying.

On the negative side, copy-pasting some commands mightn't work without some tweaks, and there's a little bit of muscle memory to get over.

On the other, when it comes to a bunch of things I find myself having a much easier time than with bash/zsh. (I'd certainly be pleased never to have to run `jq` in a bash loop again.)

As the sort of insufferable nerd who knows the difference between a hyphen, an en dash, and an em dash, and who knows how to type each (at least on macOS), I'm a bit perturbed that apparently use of em dashes is now widely seen as a sign of LLM output.

This is, honestly, the best discussion of post-quantum TLS that you’ll find https://securitycryptographywhatever.com/2025/03/23/picking-quantum-resistant-algorithms/

I can confirm that the method from https://www.nature.com/articles/s44172-024-00334-w produces nice soft-boiled eggs, although it's a bit laborious.

To save skimming the paper: they put eggs in 100°C water for two minutes, followed by 30°C water for two minutes. Repeat that cycle eight times.

(I used a sous-vide heater to keep water at 30°C, although repeatedly putting hot eggs in it pushed it a little higher over time.)

I've written several times about how to implement WebAuthn/passkey support over time. This year I decided to flesh it out a bit into a longer work on understanding and using WebAuthn

If you were at the FIDO conference in Carlsbad this year, you may have received a physical, printed booklet of the result. It took a while to get around to converting to HTML, but the text is now available:

https://www.imperialviolet.org/tourofwebauthn/tourofwebauthn.html

Recoding America is an excellent book[1] but, if you can't fit a whole book in right now, this is an excellent post by the same author to give you a flavour: https://www.eatingpolicy.com/p/bringing-elon-to-a-knife-fight

[1] https://www.recodingamerica.us/

Within a few hours we have a fancy new LLM (o1-preview). This one actually uses √acres! (Although it chickens out and converts to miles):

One can reasonably derive the √acre, a unit of distance equal to 63.61 meters. Likewise the ∛ferkin is about 34.5 cm.

(This tweet brought to you by an LLM which tried to give me a distance in acres.)

Turns out that Matthew Green could have an alternative career as a voice actor if he wanted.

https://securitycryptographywhatever.com/2024/09/06/telegram/

If you're implementing ML-DSA, do you agree with our test vectors for ML-DSA-65?

https://boringssl.googlesource.com/boringssl/+/refs/heads/master/third_party/wycheproof_testvectors/mldsa_65_standard_sign_test.json

https://boringssl.googlesource.com/boringssl/+/refs/heads/master/third_party/wycheproof_testvectors/mldsa_65_standard_verify_test.json

NIST isn't publishing end-to-end test vectors for this algorithm so we've done our best but would be very interested if anyone is interpreting the spec differently.

https://boringssl.googlesource.com/boringssl/+/0ba200173353b3f9a3527254eb16903b93170342

iCloud Keychain passkeys in Chrome on macOS: https://www.imperialviolet.org/2023/10/18/icloudkeychain.html