HN user

Kab1r

251 karma

DevOps Engineer in San Francisco

meet.hn/city/37.7707742,-122.3911712/Mission-Bay

Socials: - bsky.app/profile/kab1r.dev - discord:kabr.dev - github.com/Kab1r - linkedin.com/in/Kab1r

Interests: Climbing, DevOps, Open Source

---

Posts0
Comments138
View on HN
No posts found.

I've been building a TLA style Temporal Logic library for Verus (using LLMs). My experience so far is that LLMs are surprisingly useful at generating the mechanical proof scaffolding (when they're not occasionally trying to cheat with `assume(false)` statements), but they are not a substitute for knowing what property you actually want.

If the change is targeting a rust edition it's being treated as a feature/improvement not as a compiler bug. If there isn't a spec that explicitly says that this is expected behavior (and as far as I know there isn't a concrete spec for the rust language) it should be instead treated as a backwards compatible bug fix

I fell in love with pattern matching the first time I used Haskell. Having the feature is great, but I really don't like the syntax used here.

Last time I opted out of facial recognition when re-entering the US, I got put through an additional baggage and security scan with my passport literally locked in a box.

I have used iodine, which though isn't the easiest to setup works on every airline I have tried, to bypass airline Internet firewalls. DNS packets are one of the few things they don't seem to even try to filter. I wouldn't be surprised if you could just run wireguard over UDP/22.

the default storage options did not support ReadWriteMany for Block and Object Storage, which were necessary for using my database Postgres.

Postgres does not require ReadWriteMany volumes.

To better understand this, when I created multiple replicas, the same database could not be accessed by all the replicas. Only one at a time could access the database.

Assuming you mean multiple replicas accessing a single postgres database, this should not be a problem. I can't think of any networked database that prevents multiple clients from concurrently connecting. Postgres even has MVCC to allow multiple concurrent changes to the same record.

The architecture diagram towards the end of your blog post shows multiple subdomains, each with their own database. Each of these should be using their own RWO volume, not a single ReadWriteMany volume; that's a good way to cripple your ability to scale.

CNPG is my preferred way to manage postgres clusters on Kubernetes.