FoxQuirk 🦊 @quirk@computerfairi.es

My mom has been running a community art & poetry project using the fence around her home for the last 15+ years, which she calls The Poetry Fence. She takes it very seriously and uses it as a base for all sorts of poetry outreach in her neighborhood. She's recently written a book about her experience with this project which she's trying to get published by a small press.

And in her mid-70s, she's just created her first ever website. It'd mean a lot to her if you take a look! https://www.poetryfencecommunity.com/

She doesn't know I'm posting this, but if she did she'd probably want me to add that science is real, no person is illegal, trans rights are human rights, and banned books are worth reading. And most of all, that poetry is for everyone.

Boosts on her behalf appreciated.

#poetry #community #SmallPress #publishing

#AI

Alright fedi, can I have a recommendation for an email provider which:
- is not based in any country on earth, or at the very least, no UN-recognised nation
- has a no-log policy only in the summer, as I have a fireplace in my house so I gotta be burning those logs when it gets cold
- supports end-to-end encrypted lucid dreaming
- is completely vegan and ideally fairtrade, but rainforest alliance is also fine
- supports using other people's domains, I like those more than mine
- allows for text formatting in green, and also, ideally, red. I love my friends Green and Red.
- has diplomatic treaties with other mail providers

On Google shutting down AlphaFold.

it's a common misconception that the Windows GDI stands for “Graphics Device Interface”. it actually stands for God Damn It, because its arcanities will make you want to kill yourself

oh god rgba(255, 0, 0, 255) gets alpha-blended on Windows XP as rgb(254, 0, 0)

I need to add an epsilon 😭

A tagged subway car will always look better than one fresh from the factory. Why shouldn’t people in the city beautify their own trains? Why do we let them fill up with advertising instead?

If you're in Australia, Trans Justice is running a survey about access to and experiences with gender confirming health care, to provide data in support of their work pushing for better access. Seems designed to include DIY experiences, and those who want access but have yet to get any care. Open to all trans and gender diverse people in Australia
https://transjustice.org.au/survey/
#Trans #Australia #TransgenderHealthcare

girls only want one thing and it’s for mikrotik’s dhcpv6 to say “Status: bound”

got the bit-endianness of a bitmap format wrong again award

Yes I did transcribe alt text for this. My eyes hurt now.

Okay, we have a new contender for Most AI Thing to Ever Happen

1) July 25th: someone messes around with an LLM and posts a proof of the Collatz conjecture that does, in fact, verify in the theorem prover. (The AI use is not disclosed on the github page) https://github.com/xrchz/CollatzLean

2) July 26th: several serious bugs are posted in the theorem provers, that in principle could allow a false statement to be "proven" true. They're serious, yes, but no need for panic, because you're not going to blunder into accidentally exploiting the bugs while writing a proof, probably.
https://github.com/leanprover/lean-kernel-arena/pull/81

3) July 28th: someone who was right to be very skeptical of the Collatz proof, and had the expertise to study it with a fine-toothed comb, discovered it was exploiting a bug https://github.com/leanprover/lean4/issues/14576

4) The "proof" turns out to be exploiting multiple similar but distinct bugs to pass different solver variants!

5) the human who posted the proof acknowledges the AI use and claims they did not knowingly point it towards the bugs it exploited. https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/near/613135216

Note that the proof was posted shortly before the related bug reports were posted. It is an open question if the AI found people discussing the bugs shortly before they were formally posted and "decided" to exploit them, if the AI "knew about it" as a learned strategy from the training stage (putting every single "proof" it's ever made and ever will make into profound doubt), or if it's recently been repeatedly blundering into it by sheer stupidity and that's how people noticed the bug at about the same time.

Theorem provers aren't magic, and have bugs just like all other programs. They are tools to help us double-check our reasoning. When you skip the reasoning and ask an AI to "prove" something for you that's over your head, you're entering an adversarial pact with the monkey-pawed Devil of Customer Satisfaction.

my initial source for investigating this myself: https://lipn.info/@mevenlennonbertrand/116997927457012577

Ever wished you could have multiple independent mouse cursors on your Linux machine? No?

Anyway, turns out Wayland supports that pretty well! Let me tell you what I learned:

https://blinry.org/multi-seat-wayland/

“ah, no no, that factoid about Araragi-senpai is only established in a deuterocanonical work, I'm a Protestant”

this may as well be the Bible they're gonna be unearthing new Monogatari stories for centuries to come

reading the Japanese Wikipedia article there are how many Monogatari series short stories?!

Today, #Coreboot met #FreeBSD.

https://cgit.freebsd.org/src/commit/?id=5f74217c05a99f38a31a6e4950220964595d4ac8

When I started writing FreeBSD drivers, a friend told me:

So you’re just copying Linux drivers and rewriting them for FreeBSD ? Sounds like script work.

I explained that it doesnt work like that. First you understand the hardware. Sometimes you have to reverse engineer it. Then you test it. Only after that do you submit a driver.

He replied:

Fine. Then write a driver that doesn’t exist in any operating system.

That turned into a 500 MAD bet. (MAD is Morocco’s currency, not a measure of my sanity.)

The challenge is harder than it sounds. Almost every piece of hardware already has a Windows driver, a MacOS driver, a Linux driver, or follows a standard interface.

You dont invent hardware. You find a missing need.

So I wrote a driver for Coreboot.

Normally, the kernel log starts when the kernel boots. Everything that happened before that is a mystery. You can make educated guesses, but thats all they are.

With this driver, FreeBSD can read the Coreboot log. You get to see what happened from the very first moment the machine powered on.

That is exactly how I tracked down systems where RAM training was taking far too long because of defective memory chips.

None of this would have been possible without the amazing work of the Coreboot team.

As far as I know, FreeBSD is now the first operating system with this driver.

DragonFlyBSD is next.