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
6
0
James Bennett @ubernostrum@infosec.exchange
Public

RE: infosec.exchange/@ubernostrum/

I’m still looking for resources here if you know of any (tl;dr a company threatening debt collection over an account they admit is not mine).

I suspect a single piece of correspondence on law-firm letterhead resolves this, but for every firm I've talked to the dollar amount at issue is too low to even justify talking to one of their attorneys.

0
1
0
0
0
0
0
0
0
0
20
0
0
0
0
0
0
0
0
0
0
0
7
0
Rufus @rufustheduck@mastodon.social
Public

I was made redundant a couple weeks ago. From a school I’d worked at for 15 years, They gave us 5 days notice

Fortunately, I’m a member of a union. As were all the other teachers.

Industrial Workers of the World (IWW) were with us every step of the way. They made sure it was all above board, kept our dodgy bosses in check, & even helped us negotiate an enhanced redundancy package

So if you haven’t already, join a union

Here's my cat wearing the union badge

The back of a black cat's head - with a red IWW badge resting on his neck (don't worry - I didn't pin it on)
0
0
0
0
4
0
Anne Roth @anneroth@systemli.social
Public
Shared by leyrer

Mein feministischer Blick auf Digitalpolitik gerät ja ständig in Gefahr, als Gedöns-Thema im Abseits zu landen.

Während die Jungs die richtig wichtigen Themen machen. Cyber, und so.

Und zwischendurch sind dann aber alle kurz ganz erschrocken.

Geräte immer wichtiger als Menschen.

(Ich erwähne nicht ständig den NSA-Untersuchungsausschuss. Selbst währenddessen musste ich mich immer wieder aktiv aus der Mädchen-Schublade rausgraben.)

0
1
0
0
0
0
Hacker News 50 @hn50@social.lansky.name
Public

Anthropic takes legal action against OpenCode

Link: github.com/anomalyco/opencode/
Discussion: news.ycombinator.com/item?id=4

Remove anthropic references per legal requests: Remove anthropic-20250930.txt prompt file Remove anthropic from provider hints Remove opencode-anthropic-auth builtin plugin Remove anthropic from p...

anthropic legal requests by thdxr · Pull Request #18186 · anomalyco/opencode

Remove anthropic references per legal requests: Remove anthropic-20250930.txt prompt file Remove anthropic from provider hints Remove opencode-anthropic-auth builtin plugin Remove anthropic from p...

github.com · GitHub

0
0
0
0
1
0
0
0
0
0
2
0
Anne Roth @anneroth@systemli.social
Public

Mein feministischer Blick auf Digitalpolitik gerät ja ständig in Gefahr, als Gedöns-Thema im Abseits zu landen.

Während die Jungs die richtig wichtigen Themen machen. Cyber, und so.

Und zwischendurch sind dann aber alle kurz ganz erschrocken.

Geräte immer wichtiger als Menschen.

(Ich erwähne nicht ständig den NSA-Untersuchungsausschuss. Selbst währenddessen musste ich mich immer wieder aktiv aus der Mädchen-Schublade rausgraben.)

0
1
0
0
0
0
Kris @isotopp@infosec.exchange
Public
Shared by Jan Lehnardt :couchdb:

RE: infosec.exchange/@BleepingComp

"Identity protection company fails at its sole reason for existence"

FTFY

Identity protection company Aura has confirmed that an unauthorized party gained access to nearly 900,000 customer records containing names and email addresses.

0
1
0
0
0
0
ayo @ayo@ayco.io
Public

Took kid to school
Meetings
Went to one company building
Meetings
Went to another company building
Meetings
Went home
Viteconf online
Tried to go to supermarket
Realized I forgot grocery bag
Went home, got bag
Went to supermarket, bought chicken wings
Went home
Fried chicken wings

Screenshot of health app showing I have 17k+ steps today
0
0
0
ed @ed@digipres.club
Public
Shared by Misty

journal has a call out for articles about the use of publishing:

> Contributions from any practitioner working on digital publication are welcome, regardless of the stage or sophistication of the publication’s development. This includes boutique, shoestring publications ... as well as large-scale projects that rely on institutional backing, development teams, practices, & infrastructure.

lists.clir.org/cgi-bin/wa?A2=i

LISTSERV 16.5 - CODE4LIB Archives

lists.clir.org

0
1
0
0
0
0
0
0
0
Hacker News 100 @hn100@social.lansky.name
Public

Google details new 24-hour process to sideload unverified Android apps

Link: arstechnica.com/gadgets/2026/0
Discussion: news.ycombinator.com/item?id=4

Google details new 24-hour process to sideload unverified Android apps

The "advanced flow" will be available before verification enforcement begins later this year.

arstechnica.com · Ars Technica

0
0
0
Gammitin (Ben) 💾 @Gammitin@mastodon.social
Public

Soyo SY-6VBA-133
I picked this up as faulty not working for a few pounds a while back and managed to repair it.
It's a lovely board, I've still got to get a Northbridge heatsink that the previous owner scavenged, I'll test it but not push too hard yet (heatsink ordered).

0
0
0
Gregory @grishka@mastodon.social
Public

RE: chaos.social/@grote/1162570026

At this point I'm convinced that there's something deeply wrong with how our society treats technology.

Ruining Android for everyone to try to maybe help some rather technologically-hopeless groups of people is the wrong solution. It's unsustainable in the long run. Also, the last thing this world needs right now is even more centralization of power. Especially around yet another US company. (1/2)

0
2
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
Paul Cantrell @inthehands@hachyderm.io
Public

Just as we are entering the riskiest part of the sort of period when such capital requirements might prove salutary…

theguardian.com/business/2026/

US moves to soften capital rules: ‘Big banks can declare mission accomplished’

Fed officials expected to lower capital requirements for banks such as Goldman Sachs and JPMorgan Chase by 4.8%

www.theguardian.com · the Guardian

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

Formal verification of axiom-free gödelian ontological argument and trinity necessity proof in Isabelle HOL. ~ Yong-Dock Kim. isa-afp.org/entries/Axiom_Free

Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity Necessity Proof in Isabelle HOL

Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity Necessity Proof in Isabelle HOL in the Archive of Formal Proofs

isa-afp.org

0
0
0
FreeBSD Foundation @FreeBSDFoundation@mastodon.social
Public
Shared by Stefano Marinelli

We’re proud to share that Deb Goodkin, Executive Director of the FreeBSD Foundation, will be speaking at Open-Source Summit North America, hosted by the Linux Foundation.

📍 Tuesday, May 19, 2026, | 11:00am – 11:40am CDT | Room 101H

If you’re attending Open-Source Summit North America, we encourage you to join the session and connect with us.

Deb's talk: osselcna2026.sched.com/event/2

We look forward to seeing you there.

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

Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. arxiv.org/abs/2603.17457

arXiv logo

Synthetic Differential Geometry in Lean

This article is about the formalization of synthetic differential geometry with the Lean proof assistant and the mathematical library mathlib. The main result we prove and formalize is a Taylor theorem for functions of several variables, where the series expansion is around an infinitesimal neighborhood. Most of our proofs are in fact new. Our investigations highlight the possibility of using mathlib to do constructive mathematics.

arxiv.org · arXiv.org

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

Formalizing the classical isoperimetric inequality in the two-dimensional case. ~ Miraj Samarakkody. arxiv.org/abs/2603.14663v1

arXiv logo

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

We present a formal verification of the classical isoperimetric inequality in the plane using the Lean 4 proof assistant and its mathematical library Mathlib. We follow Adolf Hurwitz's analytic approach to establish the inequality $L^2 \ge 4πA$, which states that among all simple closed curves of a given perimeter $L$, the circle uniquely maximizes the enclosed area $A$. The formalization proceeds in two phases. In the first phase, we establish the Fourier-analytic foundations required by Hurwitz's approach: we formalize orthogonality relations for trigonometric functions over $[-π,π]$, Parseval's theorem for classical Fourier series, uniform convergence of Fourier partial sums via the Weierstrass M-test, term-by-term differentiability, and Wirtinger's inequality. In the second phase, we carry out Hurwitz's proof itself: working with simple closed $C^1$ curves given in arc-length parametrization, we reparametrize over $[0,2π]$, establish the shoelace area formula, apply integration by parts, invoke the AM--GM inequality, apply Wirtinger's inequality, and use the arc-length constraint to derive the bound $A \le L^2/(4π)$. We discuss the key formalization challenges encountered, including the interchange of infinite sums and integrals, term-by-term differentiation, and the coordination of different indexing conventions within Mathlib. The complete formalization is available at https://github.com/mirajcs/IsoperimetricInequality

arxiv.org · arXiv.org

0
0
0
David Chisnall (*Now with 50% more sarcasm!*) @david_chisnall@infosec.exchange
Public
Shared by ✧✦Catherine✦✧

A few of the things I've learned in the run up to taping out our first chip that working with FPGAs had not prepared me for (fortunately, the folks driving the tape out had done this before and were not surprised):

  • There's a lot of analogue stuff on a chip. Voltage regulators, PLLs, and so on all need to be custom designed for each process. They are expensive to license because they're difficult to design and there are only a handful of companies buying them. The really big companies will design their own in house, but everyone else needs to buy them. The problem is that 'everyone else' is not actually many people.
  • Design verification (DV) is a massive part of the total cost. This needs people who think about the corner cases in designs. The industry rule of thumb is that you need 2-3 DV engineers per RTL engineer to make sure that the thing that you tape out is probably correct. In an FPGA, you can just fix a bug and roll a new bitfile, but with custom chip you have a long turnaround to fix a bug and a lot of costs. This applies at the block level and at the system level. Things like ISA test suites are a tiny part of this because they're not adversarial. To verify a core, you need to understand the microarchitecture-specific corner cases where things might go wrong and then make sure testing covers them. We aren't using CVA6, but I was talking to someone working on it recently and they had a fun case that DV had missed: If a jump target spanned a page boundary, and one of those pages was not mapped, rather than raising a page fault the core would just fill in 16 random bits and execute a random instruction. ISA tests typically won't cover this, a good DV team would know that anything spanning pages in all possible configurations of permission and presence (and at all points in speculative execution) is essential for functional coverage.
  • Most of the tools for the backend are proprietary (and expensive, and with per-seat, per-year licenses). This includes tools for formal verification. There are open-source tools for the formal verification, the proprietary ones are mostly better in their error reporting (if the checks pass, they're fine. If they don't, debugging them is much harder).
  • A lot of the vendors with bits of IP that you need are really paranoid about it leaking. If you're lucky, you'll end up with things that you can access only from a tightly locked-down chamber system. If not, you'll get a simulator and a basic floorplan and the integration happens later.
  • The back-end layout takes a long time. For FPGAs, you write RTL and you're done. The thing you send to the fab is basically a 3D drawing of what to etch on the chip. The flow from the RTL to the 3D picture is complex and time consuming.
  • On newer processes, you end up with a load of places where you need to make tradeoffs. SRAM isn't just SRAM, there are a bunch of different options with different performance, different leakage current, and so on. These aren't small differences. On 22fdx, the ultra-low-leakage SRAM has 10% of the idle power of the normal one, but is bigger and slower. And this is entirely process dependent and will change if you move to a new one.
  • A load of things (especially various kinds of non-volatile memory) use additional layers. For small volumes, you put your chip on a wafer with other people's chips. This is nice, but it means that not every kind of layer happens on every run, which restricts your availability.
  • I already knew this from previous projects, but it's worth repeating: The core is the easy bit. There are loads of other places where you can gain or lose 10% performance depending on design decisions (and these add up really quickly), or where you can accidentally undermine security. The jump from 'we have RTL for a core' to 'we have a working SoC taped out' is smaller than going to that point from a standing start, but it's not much smaller. But don't think 'yay, we have open-source RTL for a RISC-V core!' means 'we can make RISC-V chips easily!'.
  • I really, really, really disapprove of physics. It's just not a good building block for stuff. Digital logic is so much nicer.
0
6
0
0
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Formalization of QFT (quantum field theory). ~ Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim. arxiv.org/abs/2603.15770v1

arXiv logo

Formalization of QFT

A foundational result in constructive quantum field theory is the construction of the free bosonic quantum field theory in four-dimensional Euclidean spacetime and the proof that it satisfies the Glimm-Jaffe axioms, a variant of the Osterwalder-Schrader axioms. We present a formalization of this result in the Lean 4 interactive theorem prover. The project is intended as a proof of concept that extended arguments in mathematical physics can be translated into machine-checked proofs using existing AI tools. We begin by introducing interactive theorem proving and constructive quantum field theory, then describe our formalization and the design decisions that shaped it. We also explain the methods we used, including coding assistants, and conclude by considering how AI assisted formalization may influence the future of theoretical physics. Our original release assumed three results, Minlos' theorem, the nuclear property of Schwartz space, and Goursat's theorem. In subsequent releases from our group and from contributors from the Lean community, these assumptions have been proven (or avoided), so that the OS/GJ axioms are now proven using only Lean and its library Mathlib.

arxiv.org · arXiv.org

0
0
0
0
0
0
0
0
0