Pinned toot

So the CEO of online ads giant IAB made a pretty… remarkable speech, saying:

"These extremists (referring to privacy advocates) are political opportunists who’ve made it their mission to cripple the advertising industry and eliminate it from the American economy and culture."

And this, friends, is our mission statement RIGHT THERE.

memes liberated from work

stolen from the leanprover zulip chat: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slow.20.60positivity.60/near/322881360

The notion of model of intuitionistic propositional logic (IPL) I'm

most familiar with (being a category theory/PL nerd) is a Heyting

algebra (HA): a poset with finite meets, finite joins and a Heyting

implication. If you add propositional variables, the model includes a

choice of how to interpret them as elements of the HA and if you

include axioms, their interpretation must be true in the HA.

Then you can interpret every proposition of IPL as an element of the

HA where you interpret conjunctions as meets, disjunctions as joins

and implication as the Heyting implication. If G |- A is provable then

/\ [G] |- [A] is true.

If you look up what a model of IPL is though, you'll likely find

Kripke models, and they look at first a bit different: It's a pair of

a poset W, and a "forcing relation" ||- between elements of W and

propositions of IPL satisfying a bunch of properties:

1. for variables x, if w ||- x and v <= w then v ||- x

2. w ||- p /\ q iff w ||- p and w ||- q

3. w ||- true is true

4. w ||- p \/ q iff w ||- p or w ||- q

5. w ||- false is false

6. w ||- p => q iff for any v <= w if v ||- p then v ||- q

Despite the cosmetic difference, Kripke models are instances of the HA

model construction. Given a poset W, the HA in question is

Prop^(W^op), the poset of antitone functions from W to Prop

(classically, Prop is just the boolean order 0 <= 1). This has the

pointwise ordering: f <= g if for every w. f w implies g w.

This is a Heyting Algebra:

top w iff true

(f /\ g) w iff f w and g w

bot w iff false

(f \/ g) w iff f w or g w

(f => g) w iff for any v <= w. if f w then g w

Then an interpretation of the propositional variables in this HA would

be an assignment for each variable X and w a proposition [x] w that is

antitone in w: if [x] w and v <= w then [x] v. Then the model HA

interpretation defines exactly our Kripke forcing semantics. It

defines for each proposition of IPL p a function from W to Prop that

is antitone, i.e., [p] : W^op -> Prop. Then the definition of Kripke

model is just an infix notation for this semantics:

w ||- p := [p] w

And if you unravel the definitions of the HA semantics and the HA

structure of the poset, you reproduce exactly the definition of a

Kripke model.

Bonus: this is all a "de-categorification" of a similar situation for

lambda calculus. The Kripke models are presheaf categories and the HA

are bi-cartesian closed categories.

Working with Tusky has reminded me how great open source is if you're a programmer: If something's broken, you can just fix it. This is something you rarely notice on Android because Android itself, and all official Android apps, are a kind of pseudo-open-source where the source is available but it's real hard to build outside Google. You have to download Google's git extension tool and then clone *all of AOSP* to one app. They assume you're $GOOG internal and have access to the network drives.

a re-creation of Dark Sky (weather website/API) based on open data was released today! 🌤️

https://merrysky.net/

https://pirateweather.net/

Coming soon to #foot

pipe-command-output, a new "pipe terminal output to program(s) of your choice" key binding: https://codeberg.org/dnkl/foot/pulls/1237

Before this, we had pipe-visible, pipe-scrollback and pipe-selected.

pipe-command-output pipes the last command's output. For this to work, it requires shell integration; the shell needs to emit FTCS OSC sequences to signal command output start and end. See PR for details.

When I worked at #ICANN years ago there were these great pictures of early networking and Internet typologies on the wall at the main office.

You could no longer get them from the publisher, so I took pictures! Here they are in the order referred to in the final two pictures [1/2]:

- née
- @migratory@banana.dog

- née
- @martensitingale@anti.energy

what's a bird but a word

Joined Jul 2022