Hacker News: abiro

New comment by abiro in "Anatomy of a Lean proof for software engineers"

abiro — Sun, 04 Oct 2026 12:11:56 +0000

Thanks for the feedback, it should be better now.

Anatomy of a Lean proof for software engineers

abiro — Thu, 01 Oct 2026 18:53:28 +0000

Article URL: https://agostbiro.net/posts/2026-10-anatomy-of-a-lean-proof/

Comments URL: https://news.ycombinator.com/item?id=49925602

Points: 131

# Comments: 78

We're Gonna Need More Mathematicians

abiro — Fri, 25 Sep 2026 16:36:12 +0000

Article URL: https://terrytao.wordpress.com/2026/09/24/were-gonna-need-a-lot-more-mathematicians/

Comments URL: https://news.ycombinator.com/item?id=49846751

Points: 13

# Comments: 2

The Proof in the Code: How a Truth Machine Is Transforming Math and AI

abiro — Sun, 20 Sep 2026 18:43:05 +0000

Article URL: https://www.publishersweekly.com:443/9780374620059

Comments URL: https://news.ycombinator.com/item?id=49778672

Points: 1

# Comments: 0

Liveness Proofs in Veil, Part I: The First Step

abiro — Sun, 06 Sep 2026 15:12:32 +0000

Article URL: https://proofsandintuitions.net/2026/06/24/liveness-proofs-in-veil-part-1/

Comments URL: https://news.ycombinator.com/item?id=49587263

Points: 4

# Comments: 0

New comment by abiro in "Herdr is joining Y Combinator. The runtime stays open"

abiro — Fri, 07 Aug 2026 14:17:30 +0000

For the tmux crowd: please consider sponsoring the author

https://github.com/nicm

https://liberapay.com/tmux

Formal Verification of Cryptographic Protocol Implementations in Rust

abiro — Thu, 30 Jul 2026 14:20:59 +0000

Article URL: https://dl.acm.org/doi/epdf/10.1145/3719027.3765213

Comments URL: https://news.ycombinator.com/item?id=49110419

Points: 2

# Comments: 0

New comment by abiro in "EU bans the destruction of unsold apparel, clothing, accessories and footwear"

abiro — Mon, 16 Feb 2026 11:36:31 +0000

A lot of the apparel being destroyed is unsold inventory of up-market brands to protect their pricing power. If they shipped that to less affluent countries for destruction, it's unlikely that they'd be destroyed, because those items would fetch a good price on the black market.

Zero Knowledge Encryption: Analysis of Three Cloud-based Password Managers

abiro — Mon, 16 Feb 2026 11:25:28 +0000

Article URL: https://eprint.iacr.org/2026/058

Comments URL: https://news.ycombinator.com/item?id=47033751

Points: 3

# Comments: 0

New comment by abiro in "Rust Cryptography Should Be Written in Rust"

abiro — Sat, 26 Aug 2023 19:10:31 +0000

I thought it weird that the post didn’t mention RustCrypto. It’s legit.

New comment by abiro in "Tarsnap outage postmortem"

abiro — Thu, 27 Jul 2023 08:43:29 +0000

> The second step failed almost immediately, with an error telling me that a replayed log entry was recording data belonging to a machine which didn't exist. This provoked some head-scratching until I realized that this was introduced by some code I wrote in 2014: Occasionally Tarsnap users need to move a machine between accounts, and I handle this storing a new "machine registration" log entry and deleting the previous one

Recommend writing a TLA+ model to catch stuff like this

New comment by abiro in "The past is not true"

abiro — Thu, 20 Jul 2023 12:54:50 +0000

What to read on the slice universe?

New comment by abiro in "Passkeys now support external providers"

abiro — Tue, 06 Jun 2023 09:59:26 +0000

Any details on how passkeys sync using external providers?

AMA with a WoW botter / gold seller

abiro — Sun, 28 May 2023 19:40:53 +0000

Article URL: https://old.reddit.com/r/classicwow/comments/13rgbzi/i_am_a_botter_gold_seller_at_the_start_of_every/

Comments URL: https://news.ycombinator.com/item?id=36107065

Points: 2

# Comments: 0

New comment by abiro in "Smol Developer"

abiro — Wed, 17 May 2023 07:39:57 +0000

Very cool project, congrats to the author!

Baaed on the comments, I feel that people are both under and overestimating this. On the one hand it replaces the manual tasks of searching for a template and then googling errors and this is huge! It completely disrupts search on the internet as we know it. On the other hand it won’t be able to solve problems that you couldn’t just google anyway, since that’s what it basically does under the hood.

Why the golden ratio is mostly non-sense by a Fields Medal winner [video]

abiro — Sun, 14 May 2023 12:19:46 +0000

Article URL: https://www.youtube.com/watch?v=pVKhDtOjji8

Comments URL: https://news.ycombinator.com/item?id=35937431

Points: 4

# Comments: 0

Free42 – An HP-42S Calculator Simulator

abiro — Thu, 11 May 2023 10:25:03 +0000

Article URL: https://thomasokken.com/free42/

Comments URL: https://news.ycombinator.com/item?id=35900205

Points: 80

# Comments: 35

Exploring Ethereum Token Transfers with TLA+ for Wallet Security

abiro — Sun, 16 Apr 2023 07:06:36 +0000

Article URL: https://sealvault.org/blog/2023/04/token-transfer-tla/

Comments URL: https://news.ycombinator.com/item?id=35587920

Points: 1

# Comments: 0

How do you reason about a probabilistic distributed system? (2020)

abiro — Sat, 04 Mar 2023 10:36:23 +0000

Article URL: https://ahelwer.ca/post/2020-09-11-probabilistic-distsys/

Comments URL: https://news.ycombinator.com/item?id=35019879

Points: 3

# Comments: 0

New comment by abiro in "Automerge 2.0"

abiro — Tue, 31 Jan 2023 11:21:34 +0000

Another thing to keep in mind is that if you want the data to be end-to-end encrypted, then you need both devices to be online at the same time to sync with Automerge.