Mike Mol

Flat-earthers' philosophy has its roots in the rejection of others' observations as normative; a thing must be observed by the self, directly, or it is not substantive. As such, all arguments made by someone other than oneself can be rejected as not directly observed by oneself.

This effectively becomes Not-Invented-Here syndrome as applied to epistemology.

Don't make it hard to do the wrong thing. Make it hard not to do the right thing eventually. #devops

There are two kittens behind me chasing each other with the zoomies...on a slippery floor. I'm imaging them playing mario kart in battle mode.

a cosin is just a sin from which you averted your eyes.

I've been listening to Nine Inch Nails' "I know You Can Feel It" from the Tron: Ares soundtrack. and the more I pick up on the lyrics and place them in the context of the plot, the more I realize that Tron: Ares is amazingly layered and is what the Ghost in the Shell movie *should* have been.

(slow, single-tap ride cymbal, neon reflecting off wet asphalt)

They handed me a type signature like a key to a room that didn't exist. “Total,” they said, their voice smooth as polished marble. “Well-founded.”

But I looked under the floorboards. I saw the unsafeCoerce bleeding through the floorboards like engine oil. I saw the termination checker getting paid off under the table with an structural decrease that was just a pointer trick in a cheap wig. They call it an escape hatch. I call it a structural identity theft.

You don’t get to claim the universe is constructive while you’re running a side-hustle in classical logic behind the dumpster. If the term doesn't normalize, baby, your proof is just an infinite loop wearing a halo.

Every time LinkedIn shows me an ad to work of Customs & Border Patrol (you know, human rights violation central here in the US), I report the ad as for a dangerous or extremist organization. I've had to do that twice now...

Too much #math . I misread "update todos" as "update topos"

Yup. Basement's going to flood tonight for the fourth time this calendar year...

I appreciate that greek yogurt is sufficiently dairy to use as a substitute for milk in my cereal. Less splashy and doesn't make things soggy, either.

Making "don't perform premature optimization" more rigorous:

First, you need to graph the formal coboundary of your problem. Only once you've done that is it safe to contract your graph around your actual obligation cells.

This is often called "waterfall".

If the problem is moving too fast to do that, you need to start with a smaller part of the problem, but apply the same rigor. And then compose, gluing the next cell, which you will have constructed equally rigorously.

*This* part is called "agile".

If it's real, then it must be designed,
Constructible, reachable mind.
If it cannot be seen,
Or covered, I mean,
It’s a distinction that's better declined.

I find this very useful in prompts:

```
If a distinction is real, it must be constructible; if constructible, it must be behaviorally reachable; if reachable, it must be observable; if observable, it must be coverable; if not, it is not a valid runtime distinction.
```

Give it a try as a prefix to something else.

"cybromaniac" : noun : Individual with an irresistible urge to partner with #AI on productive tasks. Portmanteau of "cyber" and "pyromaniac".

#gabion now analyzes its own repository identifies any symbols which aren't in use (or aren't in use except called by tests, or aren't in use except in aliases, or aren't in use except as re-exports...), identifies which symbols would _become_ not-in-use if those were removed, and provides a nice unified diff to for you to try if you've got git stash handy and are feeling lucky.

Verse 2 Take $S_3$, impossible to ignore A permutation group to explore We twist the Sylow-3 A brand new algebra to see...

Pre-Chorus 2 I know the axioms like before But standard bases are an absolute bore Because the twist came through $\alpha(g, h)$ is pulling us through...

Chorus And then I evaluate and see Preserving associativity! $\alpha(g, h)\alpha(gh, k)$ It balances out perfectly!

Outro Ah-ah, oh-oh A bank-shot off causality Ah-ah, oh-oh Just twisted group topology Ah-ah, oh-oh...

The name "Benoit B Mandelbrot" is a quine.

Just read through https://daniel.haxx.se/blog/2026/04/22/high-quality-chaos/

I've reached the point where I don't think it matters what programming languaeg you use to solve a given job. Use untyped lambda calculus for all it matters. Your type-checking problem has extended beyond the boundaries of what we think of as belonging to programming languages.

At this point, people need to be talking about invariants. "Principle of least surprise" is a soft invariant. "Must not write past the end of the buffer" is an invariant. "Must not write to memory or storage not set aside for the purpose" is a higher-order invariant--a dependently-typed one.

More on this later. There's a real risk of waterfall-style planning, but I don't think it has to be that way.

It's one thing to know how to do something. It's another to know why it's done that way.

The latter is the context required in order to work around obstacles safely.

#ai is really good at "knowing" how to do something. It's really bad once the skill level required goes beyond tutorial blogs and stackoverflow.

With apologies to Weezer.

Oh yeah.
All right.
Some open cover
Is mapping to nothing
My Betti number
Is filling with dread
Guess I'll just close the set.

Oh yeah, all right, the void inside
Look at the sequence, wrestle with Sartre
Meaning is empty behind my back
The complex is ready to blow.

Say it ain't closed!
This loop is a soul-breaker
Say it ain't closed!
The void is a space-taker.

I can't compute you
I never could prove
That which might bound you
So try to resolve
When I say
This space is a manifold away from me
That strips the meaning every day
So resolve.

Say it ain't closed!
This loop is a soul-breaker
Say it ain't closed!
The void is a space-taker.

Dear de Rham, I write you
In spite of empty spaces
You mapped out the cycles, found the truth or so I hear
This torsion awakens existential dread and fear
The zero, the one-form, the self is drowning in the void!
Yeah, yeah-yeah, yeah-yeah!

(Maximum volume)
Say it ain't closed!
This loop is a soul-breaker
Say it ain't closed!
The void is a space-taker.
Say it ain't closed!
Say it ain't closed!

I just had a funny mental image of taking the old Win32s drawing API and replacing the idea of a uniform field of pixels with a sparse lattice of nedges.

I've learned that the annoyance of perpetually out-of-date codelabs extends to skills.google labs, too. "(virtual proctor like thing): Set up a vm instance" "(instructions saying to do this): (not found)"

"No obligation with hasDischargeQuery found -- the system cannot witness its own discharge"

#phrasing

The more I try showing my family videos about category theory and abstract algebra, the more I realize everything out there is terrible, pedagogically speaking, and I want to make my own.

With apologies to Eric Claptopn...

Would you know my class
If I met you in loop space?
Would it be the same
If I mapped you in loop space?
I must preserve
The points and curves
'Cause I know this path belongs
Here in loop space.

Would you hold the line
Through a smooth deformation?
Would our bounds align
Through a smooth deformation?
I'll map my way
From X to A
'Cause I know this curve can't stay
In a fixed state.

Spaces shrink you down
To a single point
Cuts will break apart
Leave the loops disjoint
Loops disjoint...

Beyond the sphere
The type is clear
And I know there'll be no more
Gaps in this space.

Would you know my class
If I met you in loop space?
Would it be the same
If I mapped you in loop space?
I must preserve
The points and curves
'Cause I know this path belongs
Here in loop space.

'Cause I know this path belongs...
Here in loop space.

I have an LLM writing python code so that an LLM can write lua code to manage experiments around hyperparameters so that two LLMs can adversarially argue about the structure and clarity of formal language so that a script can draw a graph of Toulmin arguments and weaknesses so I can audit my own formal writing. (And only that outermost LLM is running in a datacenter anywhere; the rest is small enough to run on my laptop).

What is my life? #ai

With apologies to No Doubt:

In the reals we felt so safe
One axis, rules we could trace
Then doubles came along at night
Pairs of pairs, still felt just right

But every time we cross that line
A mirror flips, a twist in sign

Don’t *fold*, I know what you’re extending
Every step breaks what we’re defending
From fields to things that only pretend
To behave the way we planned them

Complex planes, a spinning phase
i squared laughing at our ways
Quaternions start to bend the scene
Order’s gone, but norms stay clean

Noncommuting, turning cold
Still the length can’t be sold

Don’t *fold*, I know what you’re constructing
Rules decay but you keep doubling
Closure’s fading, hands unbend
This is the Cayley–Dickson end

Octonions, cracks appear
No associating here
Sixteen dims, we lose the thread
Zero divisors raise the dead

We had a group
Then a ring
Then something else entirely

Don’t *fold*, I know why you’re insisting
Every loss is mathematically consistent
You trade the laws you used to defend
For one more doubling step again

I won’t speak
I’ll just extend
One more time
…and break a friend

There’s Girard for the resource we spend,
And Heyting for growth without end.
The Boolean close,
As everyone knows,
Is where the Deductions descend.

What is it with the quality of barrel connectors these days? Two different products, two different cable/strain designs, four months apart, same failure mode. In this case, the appliance (a bike battery) fell several inches onto the cable. In the other case, the barrel broke when I moved the appliance (an electric litter box). Literally the first two such failures I've ever seen.

You know the classic party game Twister? Here's Twister for hackers:

Everyone starts off with 16 symbols. Every round, a program synthesizes a (mostly) random unit test around interacting with one or more of those 16 symbols. Every player's program has to pass all unit tests within a time limit, at which point a new random unit tetst will be added.

Anybody remember the old TLC game Robot Odyssey?

I just imagined a reboot of that, but where you wire up everything in Verilog instead of as a discrete soldering exercise.

With apologies to Black Sabbath:

Weights are gathered in their clusters
Just like nodes in dense adjusters
Tensors plotting back-induction
Optimizers for production
In the racks the silicon's churning
As the training loop keeps turning
Minimizing loss and finding
Local optima they're grinding
Oh lord yeah!

Top-down parsers hide themselves away
They only triggered the call
Recursive descent leads the way
And pushes the stack to the wall!
Grammar’s left to the core
Time complexity’s the war, yeah!

Now the Markov Chain is turning
Random samples always yearning
Sampling space to find the poise
Stochastic truth within the noise
No more clusters have the power
Carbon heat has struck the hour
Cooling systems start to sour
Grid is failing by the hour
Oh lord yeah

If the hand wants the hand, and the eye the eye, I wonder what the head wants, by and by.

Ohh, the head of vecna. Less famous than the rest. But I'll tell you a secret; the more they put it to the test, the less that anybody knows.

I wonder how a thing like that goes?

So this was funny. My solver rederived theorems that had been marked as private because it predicted they'd be there. Twice. #agda

```
-- Made public 2026-05-02 (Step 1 of orbit-aware-completion-residue
-- arc): NSAHomReal2Complex re-derived `α*0` / `0*α` / `neg-0`
-- inline; Goal-T's `*-comm-ℂ` proof would re-derive them again.
-- Two re-derivations of identical content trigger RFS to expose
-- the originals. Behavior-preserving for existing callers.
```