Meetups/Infra/2026-03-09

Tony Hoare memorial day--Communicating Sequential Processes, Hoare logic/triples, relation to compilers + security + leveraging alongside ai tools to maintain key guarantees.

Topics

• Tony Hoare --

Introductions

• [name] - [background]. [goals for meetup, or interests to explore]

• Loren - background in cloud engineering and scraping, distributed systems
• Chris - web scraping, banging my head against problem of scraping events online
• Renaud - recent grad, interest in infra, homelab,
• Hey - likes the idea of freedom
• Dave - worked with systems workflow systems, a little go, seen a lot of distributed systems.
• Atul - project management, last programming 25 years ago, hardware accel at xylinx, robot startup for manufacture, recent got a desktop for running local LLM
• Derek - Petri-nets
• Jason - grad many years ago, software engineer, complexity of software as it grows, how to rethink that.
• Janus - Data engineer, interest in hardware
• Dan - hacking on cuda,
• Doug - likes writing software, likes computers and conversing here at the meetup
• Max - tired, here to rest, homeserver stuff is cool
• Zacchae - interest in infrastructure, managed compute is scarce things, lowering the barrier to netry, freedom of control over compute
• Josh - hasn't programmed in a long time, likes playing with computers and hanging out
• Jet - software extremist, thinks the gate is unplugged.
• Veronica - working on replacing github
• Jacob - exploring design space, rewiring graph that represents code with LLMs.
• Robert - likes playing with GUI's modifying devices, network attached storage. Likes to test out operating systems.

Lesson or Demo

• Read aloud: clarify for meetup. We are taking notes in a riseup pad (or I am--help appreciated, and links). We have meeting notes posted to the wiki. noisebridge.net, search Infra, or Meetups

Broken cable https://photos.app.goo.gl/nRMAnjGgMBLCn47H6

/Infra. (the Infrastructure page has a disambiguation link.)

• Shell, web services, self-hosting, networking!

Famous Go slogan often attributed to Rob Pike:
“Do not communicate by sharing memory; share memory by communicating.”

https://go.dev/ref/mem

This line directly reflects Hoare’s CSP philosophy.

Communicating Seqeuential Processes, C.A.R. Hoare:
https://antares.sip.ucm.es/~luis/doctorado06-07/cspbook.pdf

CSP concept                        Go feature
------------------------------     ----------
Process                            goroutine
Channel communication              chan
Select over multiple channels      select statement

* The Tail at Scale: https://dl.acm.org/doi/pdf/10.1145/2408776.2408794
 Even rare performance hiccups affect a significant fraction of all requests in
 large-scale distributed systems.
 Great Strange Loop talk on this research -- https://www.youtube.com/watch?v=_Zoa3xkzgFk&themeRefresh=1 

Eliminating all sources of latency variability in large-scale systems is impractical,  especially in shared environments.

Using an approach analogous to fault-tolerant computing, tail-tolerant software techniques form a predictable whole out of less-predictable parts.


Concurrency - in hardware. Adders, sequential carry. 

Clojure --

Jason:  The more I deal with distributed systems, the more I find myself reaching for systems that enforce contraints up front, and let me build freely within the constrained system, [not having to mix buisness logic with artful conventions that need to maintain invariants of the system, across time, and widely-distributed servers.]

Loren: there's a connection here with AI—--precommiting to constraints up front, lets you fight the model visibly, instead of shadowboxing with correctness.

Jason:  Operating: systems, that is, the operation of systems, is way harder that writing software

Veronica:  For LLMs, it matters what systems you're translating among, from or two.  If the invariants are similar, obvious, explicit, local--then 

There's lots in the code, implicitly tweaked behavior piled on over years.


COBOL, started with manual source management, duplicated systems.

Sort algorithms

bogosort, while not sorted: randomize list. Is it sorted?


Close reading of Tony Hoare wikipedia page, 2nd paragraph.

Quicksort, 
- randomize

https://www.tumblr.com/accidentallyquadratic

Fun visualizaer of sorting algorithms: https://www.cs.usfca.edu/~galles/visualization/ComparisonSort.html

TigerBeetle -- does 
Clojure
 Datomic -- 
 Cognitect
NuBank

Jepsen.io 

Deterministic VM for testing and shrinking:
https://www.youtube.com/watch?v=_xJ4maWhSNUd
https://sqlsync.dev/posts/antithesis-driven-testing/
https://antithesis.com/


Papers We Love

Mutable state is the root of all evil

• https://www.recurse.com/blog/51-paper-of-the-week-out-of-the-tar-pit

HOARE Logic: Practical uses:

Verified compilers — CompCert (a formally verified C compiler) uses Hoare-style reasoning to prove the compiler doesn't introduce bugs Operating system kernels — seL4 is the most famous example, a microkernel with a full formal correctness proof Safety-critical systems — aerospace, medical devices, nuclear systems where a bug can be catastrophic Cryptographic code — projects like HACL* formally verify cryptographic primitives (used in Firefox, Linux) Smart contracts — verifying Ethereum contracts behave as specified, since bugs are exploitable and irreversible In academia/tools:

Separation logic (an extension of Hoare logic) is heavily used to reason about pointer-manipulating programs and concurrent code Tools like Dafny, Frama-C, VeriFast, and Iris are built on Hoare-style reasoning Coq and Isabelle proof assistants frequently use it

Jet - Could I show how I deploy nix modules of things? it's cool I promise <3

Outros

• Chris --
• Renaud -- cool to learn about you implementation of git
• Robert -- did not learn anything today -- confusing
• Dave -- cool git, didn't know about Hoare notations
• Derek -- cool git, Hoare logic, ...
• Jason -- git cool, excited to watch, video when home: from unit tests ... to the whole universe
• Janus -- git rewrite, p cool -- reverse engineers. Hoare logic, pretty cool--will
• Dan -- will be watching the video too
• Doug -- git cool, won't be watching the video
• null -- just arrived
• Max -- sorting algorithms are cool, didn't attend to the rest
• Zacchae -- I was lisping too hard, idk. Cool to see the git thing. And audio for the sorting.
• Josh -- installed steam on my laptop
• Jet -- happy with what I saw, so happy that you came. Not excited to re-clim
• Veronica -- sorting alg, cool. Quantum bogo sort. V cool. Just pray.
• Jacob -- no,

• Loren --

same people, papers we love, 1x/mo, Antithesis people

Questions, Discussion, or Coworking

• [Issue]

For next time

Questions

Fun projects:

   - Ceph FS
   - Spark shard-manager
   - does anyone use m3?]]]

Readings & Exercises

• Readings
• Exercises

Join online

• Try it yourself!
  • Join libera.chat #nb-meetup-infra

https://www.noisebridge.net/wiki/Meetups/Infra