What is Hackers' Pub?

Hackers' Pub is a place for software engineers to share their knowledge and experience with each other. It's also an ActivityPub-enabled social network, so you can follow your favorite hackers in the fediverse and get their latest posts in your feed.

0
0
0
0
0
0
dan @danabra.mov@bsky.brid.gy
Public

part of it is i just don't have any mental model for what actually happens when it's off and then on like does soundness REQUIRE catching up on every firehouse event? or does soundness not require it but "resync everything missed" could be expensive? or there's no technical way to distinguish?

0
0
0
0
2
0
Tony Finch @fanf@mendeddrum.org
Public
Shared by Chris Siebenmann

from my link log —

WebPKI and you.

blog.brycekerley.net/2026/03/0

saved 2026-03-09 dotat.at/:/2I9ZS.html

WebPKI and You

There’s been a push over the last twelve years to move web traffic off unencrypted HTTP to encrypted HTTPS, to protect the general public from dragnet surveillance, gaping assholes on public wifi>airpwn, backhauls over unencrypted satellites, that kinda thing. HTTPS relies on a public key infrastructure to make sure only authorized servers have keys for specific websites. [>oid]: an OID or “Object IDentifier” is intended [brs]: https://cabforum.org/working-groups/server/baseline-requirements/documents/CA-Browser-Forum-TLS-BR-2.1.8.pdf [crtsh]: https://crt.sh/?q=blog.brycekerley.net [lol-diginotar]: https://en.wikipedia.org/wiki/DigiNotar#Issuance_of_fraudulent_certificates [iv-ocsp]: https://www.imperialviolet.org/2011/03/18/revocation.html [>mac-ocsp]: Jeff Johnson’s [>crlite]: these use cascading bloom filters which [>short-lived]: the CA/BF baseline requirements [trustico-chrome]: https://security.googleblog.com/2017/09/chromes-plan-to-distrust-symantec.html [trustico-gone]: https://arstechnica.com/information-technology/2018/03/trustico-website-goes-dark-after-someone-drops-critical-flaw-on-twitter/ [trustico-compromise]: https://groups.google.com/g/mozilla.dev.security.policy/c/wxX4Yv0E3Mk/m/o1cdfx2nAQAJ [>enclaves]: Amazon Web Services (AWS) and [>history]: i mean, i remember from when it happened [>parasite]: You may have realized that I don’t think [van-halen]: https://snackstack.net/2023/07/03/in-search-of-van-halens-brown-mms/ [>osi]: I’m not going to hit you with a [>responsibility]: in every part of your life! [>bloom]: [>later]: At time of publishing, it’s March 8, 2026 [hsts]: https://developer.mozilla.org/en-US/docs/Web/HTTP/Reference/Headers/Strict-Transport-Security [>hsts]: This is generally a hardcoded value, [>cattle]: “cattle” is when there’s [ari]: https://letsencrypt.org/2025/09/16/ari-rfc [>caddy-ari]: I checked Caddy, the front-end server [>left]: there may be value in trying to renew [audits]: https://cabforum.org/about/information/auditors-and-assessors/audit-criteria/

blog.brycekerley.net · Bryce’s Blog

0
0
0
0
1
0
Tim Bray @timbray@cosocial.ca
Public

Seems painfully obvious that, whatever you think about code, anyone using it is heading for a code-review logjam. Assuming that the org requires code review; if yours doesn’t, nothing I can say will help you. Anyhow, Rishi Baldawa writes smart stuff about the problem and possible ways forward, in ˚The Reviewer Isn't the Bottleneck”: rishi.baldawa.com/posts/review

[My prediction: A lot of orgs will *not* do smart things about this and will suffer disastrous consequences in the near future.]

The Reviewer Isn't the Bottleneck

AI tools are flooding PR queues and the instinct everywhere is to call review the bottleneck. I think that’s the wrong question. The reviewer is the last sync point before production changes. The goal shouldn’t be how to remove the gate, but how to make it cheaper to operate.

rishi.baldawa.com · Rishi Baldawa

0
1
0
Jay 🦋 @jay.bsky.team@bsky.brid.gy
Public
Shared by Tom Casavant

Some personal news: I’m transitioning from CEO to a new role as Bluesky’s Chief Innovation Officer! I’m excited to welcome @toni.bsky.team@bsky.brid.gy as our interim CEO. More here: bsky.social/about/blog/0...

A New Chapter for Bluesky - Bl...

A New Chapter for Bluesky - Bluesky

After several intense and incredible years building Bluesky from the ground up, I've decided to step back as CEO and transition to a new role as Bluesky's Chief Innovation Officer.

bsky.social · Bluesky

0
0
3
0
0
0
0
0
0
raconet @raconet@elbarri.online
Public

El 28 de febrer vam celebrar la segona fedifesta a Alacant, i va ser tot un èxit i molt interessant 😊

Una vintena de persones vam aprendre sobre el fedivers, i cam compartir dades i anècdotes sobre la nostra experiència amb les xarxes socials en general. Molta gent es va fer un compte a Mastodon, i sobretot hem fet comunitat amb persones i col·lectius d'Alacant, i compis de Citical Switch (@criticalswitch) i Múrcia (@elena, @kyva⁂ Kyva :veenk_logo:). Gràcies a totes per vindre 🧡

Per a qui no haja pogut vindre, us passem dos enllaços:
- com fer-me un compte a mastodon: sindominio.net/lafurgo/
- aprendre sobre el fedivers: critical-switch.org/ca/posts/i

També podeu seguir-nos al mastodon: @raconet, @casaltiocucCasal Popular Tio Cuc Alacant

Esperem veure-vos a la següent!

Persones assegudes en rogle dins del casal debatint i mirant una presentació projectada en la pantalla de projector.
0
1
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Implementing dependent type theory inhabitation and unification. ~ Chase Norman, Jeremy Avigad. arxiv.org/abs/2603.01463

arXiv logo

Implementing Dependent Type Theory Inhabitation and Unification

Dependent type theory is the foundation of many modern proof assistants. Inhabitation and unification are undecidable problems that are useful for theorem proving and program synthesis. We introduce Canonical-min, a sound and complete solver for inhabitation and unification in dependent type theory, implemented in 185 lines of Lean code. This paper describes a novel implementation of dependent type theory and a monadic framework to transform the type checker into a performant solver. Finally, we introduce DTTBench, a benchmark for type inhabitation in dependent type theory.

arxiv.org · arXiv.org

0
0
0
Why @why.bsky.team@bsky.brid.gy
Public

Very excited for the new projects we have in the works that Jay will now be leading more directly as CIO. She has always been excellent at seeing the vision and knowing where to go, so glad that we're unburdening her from the day to day of running the company.

RE: https://bsky.app/profile/did:plc:oky5czdrnfjpqslsw2a5iclo/post/3mgnkkbkw2c2v

0
0
0
Jay 🦋 @jay.bsky.team@bsky.brid.gy
Public

Toni has been an advisor to us for years, and it's an honor to have him come in to lead us into this next phase 🚀

RE: https://bsky.app/profile/did:plc:cwf4mmm7mpzistinx3ox2zhj/post/3mgnkln3fmk2j

Toni Schneider (@toni.bsky.team)

I'm thrilled to announce that I'll be joining Bluesky as interim CEO. I deeply believe in what this team has built and the open social web they're fighting for. More here: https://toni.org/2026/03/09/coming-off-the-bench-for-bluesky/

bsky.app · Bluesky Social

0
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Unbiasing symmetric monoidal categories in Lean. ~ Robin Carlier. arxiv.org/abs/2603.00896

arXiv logo

Unbiasing symmetric monoidal categories in Lean

We present a formalization in Lean 4, within the framework of the mathematical library Mathlib, of the unbiasing process for symmetric monoidal categories. This is realized by extending the data of a symmetric monoidal category to a Cat-valued pseudofunctor from the (2,1)-category of spans of finite sets, encoding tensor products of higher arities and their coherences. The construction relies on a formalization of Mac Lane's coherence theorem using Piceghello's presentation of free symmetric monoidal categories as symmetric lists, and uses an encoding of universal formulas via an appropriate Kleisli bicategory.

arxiv.org · arXiv.org

0
0
0
0
0
0
dan @danabra.mov@bsky.brid.gy
Public

@alex.bsky.team if Tap is the recommendation in the docs, i think it's important to not just verify that it runs, but to also verify that an actual development workflow — such as closing your laptop and then continuing work next day — also works i feel like this is an assumption that nobody tested

0
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Mathematicians in the age of AI. ~ Jeremy Avigad. arxiv.org/abs/2603.03684

arXiv logo

Mathematicians in the age of AI

Recent developments show that AI can prove research-level theorems in mathematics, both formally and informally. This essay urges mathematicians to stay up-to-date with the technology, to consider the ways it will disrupt mathematical practice, and to respond appropriately to the challenges and opportunities we now face.

arxiv.org · arXiv.org

0
0
0
0
0
0
0
0
0
IEEE Spectrum @ieeespectrum@mastodon.social
Public

Curling is at a crossroads: how much technology are we willing to incorporate into the sport, into training, and into competitions? spectrum.ieee.org/olympics-cur

Tech Is Taking Over Olympic Curling

Can the "Spirit of Curling" survive the rise of AI-powered strategy and precision?

spectrum.ieee.org · IEEE Spectrum

Link author: IEEE Spectrum@ieeespectrum@mastodon.social

0
0
0
mcc @mcc@mastodon.social
Public

What I listened to today: 2024-05-22 Mastodon post, Autechre

Sean Booth of Æ has a Fediverse account and one day last year posted this gorgeous outtake from Oversteps (which I still consider Æ's most risk-taking album). It's kind of breathtaking, utterly unlike Æ, a labyrinth of classical spanish guitar, while also quintessentially Æ and very "yeah that, that's an Oversteps track". I think of this as a cousin to known(1) but I feel shadows of other songs of that era too

data.runhello.com/blj/autechre

mcc @mcc@mastodon.social
Public
Shared by mcc

What I'm listening to today: "Southside", Lil Keke

What if I spent this entire week linking classic "dirty south" hip-hop tracks I loved from 97.9 The Box back in the 90s (which, I am visiting Houston this week and their selection is still excellent). No one could really stop me.

Here's known DJ Screw associate Lil Keke, dropping an effortless flow that stuck in my head for 29 years and my favorite instance of slide guitar in the entire corpus of music. Sorry Beck

youtube.com/watch?v=kg7cThO_vgo

Southside

Provided to YouTube by Virgin Music GroupSouthside · Lil' KekeDon't Mess Wit Texas℗ 1997 Seven13/SoSouth Music DistributionReleased on: 1997-07-01Composer Ly...

www.youtube.com · YouTube

0
0
1
0
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Formalization in Lean of faithfully flat descent of projectivity. ~ Liran Shaul. arxiv.org/abs/2603.04376

arXiv logo

Formalization in Lean of faithfully flat descent of projectivity

We formalize in Lean the following foundational result in commutative algebra: Let $R \to S$ be a faithfully flat map of (not necessarily noetherian) commutative rings, and let $P$ be an arbitrary $R$-module. Then $P$ is projective over $R$ if and only if $S\otimes_R P$ is projective over $S$. This formalizes and verifies Perry's fix of a subtle gap in the classical work of Raynaud and Gruson, a result which is a key ingredient in the study of finitistic dimension of commutative noetherian rings.

arxiv.org · arXiv.org

0
0
0
0
0
0
dan @danabra.mov@bsky.brid.gy
Public

in reality my workflow is to constantly delete tap .db file, truncate my local db tables, and do a clean resync. multiple times a day because Tap gets stuck everytime. this workflow is way worse than when i had my own ingester which at least behaved predictably and reacted instantly.

0
0
0
0
0
0
Rose 🌹 @rose.bsky.team@bsky.brid.gy
Public

So excited to welcome Toni to the Bluesky team! Toni has been an advisor to me and Jay for years, and we're thrilled he has answered our call to lead us in the interim.

RE: https://bsky.app/profile/did:plc:cwf4mmm7mpzistinx3ox2zhj/post/3mgnkln3fmk2j

Toni Schneider (@toni.bsky.team)

I'm thrilled to announce that I'll be joining Bluesky as interim CEO. I deeply believe in what this team has built and the open social web they're fighting for. More here: https://toni.org/2026/03/09/coming-off-the-bench-for-bluesky/

bsky.app · Bluesky Social

0
0
0
0
0
0
0
2
0
dan @danabra.mov@bsky.brid.gy
Public

what i need in local development: - i have ~4 users, i can ignore commits for other users - i turn it on while working on the app (obviously! it's on my laptop). i don't care what happens in between. - i'm fine with it nuking its own db and resyncing from scratch if needed - i can't "wait hours"

0
0
0
0
0
0
dan @danabra.mov@bsky.brid.gy
Public

if tap is fundamentally incapable of "running on and off" then this needs to be documented. it's just completely unclear how to use it properly. maybe the problem is between the screen and the keyboard, but it's been unusable for local development for me ever since i tried it. regret switching to it

0
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Proving and computing: The infinite pigeonhole principle and countable choice. ~ Zena M. Ariola, Paul Downen, Hugo Herbelin. arxiv.org/abs/2603.04006

arXiv logo

Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice

Structural recursion is a common technique used by programmers in modern languages and is taught to introductory computer science students. But what about its dual, structural corecursion? Structural corecursion is an elegant technique, supported in languages like Haskell and proof assistants such as Rocq or Agda. It enables the design of compositional algorithms by decoupling the generation and consumption of potentially infinite or large data collections. Despite these strengths, structural corecursion is generally considered more advanced than structural recursion and is primarily studied in the context of pure functional programming. Our aim is to illustrate the expressive power of different notions of structural corecursion in the presence of classical reasoning. More specifically, we study coiteration and corecursion combined with the classical callcc operator, which provides a computational interpretation of classical reasoning. This combination enables interesting stream-processing algorithms. As an application, we present a corecursive, control-based proof of the Infinite Pigeonhole Principle and compare it with the continuation-passing proof of Escardó and Oliva in Agda. To further demonstrate the power of mixing corecursion and control, we give an implementation of the Axiom of Countable Choice. In contrast to the usual continuation-passing implementations of this axiom, which rely on general recursion whose termination is established externally, our approach justifies termination by coiteration alone.

arxiv.org · arXiv.org

0
0
0
0
0
0
0
0
0
dan @danabra.mov@bsky.brid.gy
Public

@dholms.at is local development supported with Tap? the workflow is that i don't have it on always, i only have it on while developing. i *do not* want it to "catch up" on thousands of commits across hours or whatever. my app literally has 4 users (all of which are me). i just need live updates

0
0
0
0
0
0
0
4
0
0
0
0
Mike Piontek @robotspacer@xoxo.zone
Public
Shared by Misty

Here’s my playthrough of another important HyperCard game: Caper in the Castro by C.M. Ralph. It’s the first game to focus on LGBTQ themes. It’s a point-and-click murder mystery, and it has a lot of charm. I love it. youtube.com/watch?v=ADdfysIYFxQ

You can play it here on the Internet Archive: archive.org/details/hypercard_ The game was thought to be lost for several years; I’m so glad it was eventually recovered.

Caper in the Castro – the first LGBTQ game, made in HyperCard

Tonight I’m playing the first known LGBTQ game, Caper in the Castro by C.M. Ralph! It’s a point-and-click murder mystery made in HyperCard, released in 1989 ...

www.youtube.com · YouTube

0
0
0
0
0
1
0
0
0
0
0
0
Mike Masnick @mmasnick.bsky.social@bsky.brid.gy
Public

Toni is a wonderfully thoughtful and insightful exec, who has shown that you can build a real business around open software. Finding someone who can execute and who understands the vision of an open protocol at the same time is rare—Toni gets it. I'm excited to see what Toni and Jay build together.

RE: https://bsky.app/profile/did:plc:cwf4mmm7mpzistinx3ox2zhj/post/3mgnkln3fmk2j

Toni Schneider (@toni.bsky.team)

I'm thrilled to announce that I'll be joining Bluesky as interim CEO. I deeply believe in what this team has built and the open social web they're fighting for. More here: https://toni.org/2026/03/09/coming-off-the-bench-for-bluesky/

bsky.app · Bluesky Social

0
0
0
1
0
0
洪 民憙 (Hong Minhee) :nonbinary: @hongminhee@hollo.social
Public
Shared by 洪 民憙 (Hong Minhee) :nonbinary:

Salvatore Sanfilippo (@antirez) and Armin Ronacher (@mitsuhikoArmin Ronacher) both argue that reimplementation of libraries is fine. Their legal reasoning might be correct. That's not the point.

Legal and legitimate are different things—and both pieces quietly assume otherwise.

https://writings.hongminhee.org/2026/03/legal-vs-legitimate/

合法であれば正当か——AI再実装とコピーレフトの侵食

先週、Pythonのテキストエンコーディング検出ライブラリchardetのメンテナーであるDan Blanchardが、 新しいバージョンをリリースした 。 chardet 7.0は従来比48倍の速度を誇り、マルチコアに対応し、 設計から作り直されている。 AnthropicのClaudeが貢献者として登録されている。…

writings.hongminhee.org · 洪民憙雑記

Link author: 洪 民憙 (Hong Minhee) :nonbinary:@hongminhee@hollo.social

2
1
0
洪 民憙 (Hong Minhee) :nonbinary: @hongminhee@hollo.social
Public
Shared by 洪 民憙 (Hong Minhee) :nonbinary:

I'm thinking of proposing a /social web community track at @COSCUP 2026 (Aug 8–9, Taipei)—think FOSDEM's Social Web devroom, but in East Asia. Before I submit the CFP, I'd love to get a sense of what to call it. What do you think?

(Boosts appreciated!)

0
2
0
Venkatesh-Prasad Ranganath @orderwithchaos@mastodon.social
Public
Shared by 洪 民憙 (Hong Minhee) :nonbinary:

"Whatever courts eventually decide about AI reimplementation, the question we need to answer first is not a legal one. It is a social one. Do those who take from the commons owe something back?"

writings.hongminhee.org/2026/0

合法であれば正当か——AI再実装とコピーレフトの侵食

先週、Pythonのテキストエンコーディング検出ライブラリchardetのメンテナーであるDan Blanchardが、 新しいバージョンをリリースした 。 chardet 7.0は従来比48倍の速度を誇り、マルチコアに対応し、 設計から作り直されている。 AnthropicのClaudeが貢献者として登録されている。…

writings.hongminhee.org · 洪民憙雑記

Link author: 洪 民憙 (Hong Minhee) :nonbinary:@hongminhee@hollo.social

0
0
0
0
0
0