The time has come: Claude is able to poke holes in the dark corners of Rocq's kernel and come up with proofs of False!
The days of "our reasonable users use the unreasonable features only in reasonable ways so it's ok to have them" really are over. Can't wait until someone vibe codes a complicated proof without looking too closely at it (since it's been checked by the kernel, it must be fine!) only to later realise it was actually bogus and such a bug without the agent saying so...
extremely angry rant about puritans
Bose recently did an unambiguously good thing, by publishing the API for the audio hardware they were originally going to brick: https://www.theverge.com/news/858501/bose-soundtouch-smart-speakers-open-source
However, I've seen some people say "don't praise Bose for this, they didn't do this until there was backlash".
SHUT UP. Shut the FUCK UP. I'm DONE living in a society where you get dragged through hell if you make a mistake, EVEN AFTER YOU CORRECT THE MISTAKE. I'm so fucking tired of hearing stupid excuses for this kind of puritanism like "they should've known better" NOBODY KNOWS BETTER UNTIL *AFTER THEY MAKE THE MISTAKE*. THAT'S HOW LEARNING *WORKS*.
And before you say "Companies aren't your friend" PUNISHING THEM FOR FIXING THEIR MISTAKES WON'T MAKE THEM DO THE RIGHT THING EITHER. If other people, or companies, see someone get punished for both messing up AND fixing the mistake, they just won't bother at all!
People HAVE to be allowed to make mistakes. They HAVE to be given a chance to improve.
I wish people stopped using AI generated images in their articles and presentations. I get the temptation to break up the text, but it’s pointless to break up the text with images that don’t tell a relevant story - so regardless of what you think of genai it just adds no value at best.
If you want the text to be easier to digest and don’t have and can’t produce any sketches or screenshots, maybe add cat photos instead?
New thing from the Zstd (and LZ4/xxhash) crowd: OpenZL. A dozen or so building blocks (shufflers, transposers, filters, compressors) that can be chained together. Can automatically build "best" config based on sample data; same decompressor can decompress any config. Nice! https://openzl.org/ (and whitepaper: https://arxiv.org/abs/2510.03203) #compression #openzl
Toots as he pleases.