Metadata

In middle school I could not get through long passages no matter how hard I tried. I would read an entire page and find that nothing had registered, so I started taking notes out of desperation. This was the late 80s, and Tony Buzan's mind maps had just reached Turkey. This led me to produce pages and pages of notes that looked like spiderwebs. Creating those notes have helped me tremendously. I made sense of what I was reading by figuring out which branch they would hang off in my mind maps. I realized my pages were not for storing the information as much as they were for processing it. It took me another ten years to understand why this works so well. During a stretch of PhD procrastination, I read Manuel Blum's advice to graduate students : You are all computer scientists. You know what FINITE AUTOMATA can do. You know what TURING MACHINES can do. For example, Finite Automata can add but not multiply. Turing Machines can compute any computable function. Turing machines are i...

This NeurIPS'26 workshop paper takes TLA+ specs from GitHub, translates them into Verus, and has LLM agents prove the safety and liveness properties in the specs. The motivation The paper aims to address two problems it raises with TLA+. First, nothing ties the spec to the code, so they drift apart. And second, it claims that proof support is thin: TLC only checks small configurations, and TLAPS is weak on liveness. They abandon pursuing the first weakness they raise at the onset of the paper. Closing it needs a proof that the generated Rust code (which it turns out TLA-Verus doesn't produce anyway) refines the spec, so they list this as future work. It gets worse though. There is no refinement proof between the TLA+ spec and the Verus spec either. Nothing establishes that the translated Verus spec means what the original meant. (Trace validation, meanwhile, is a viable way of tying TLA+ to implementation code, and has been getting a lot of attention recently. ) They dedicate ...

I have come to suspect that to most people thinking is painful. Some of us are addicted to thinking. Some of us find it a necessity. Johnny enjoyed it. I even have the suspicion that he enjoyed almost nothing else. -- Edward Teller, eulogizing John von Neumann I listened to Ananyo Bhattacharya's " The Man from the Future: The Visionary Life of John von Neumann " in my car during the many commute hours Bay Area traffic afforded me. I thought I should share the Johnny phenomena here. I knew about von Neumann being a very influential mathematician/scientist/engineer but the full list still left me bedazzled. In his 53 years of life (1903-1957), von Neumann seeded so many fields. Every time there was an important discovery in physics, mathematics or computation, John von Neumann was there. Set theory and the foundations of mathematics. The mathematical formulation of quantum mechanics. Operator algebras (still called von Neumann algebras). Ergodic theory. Game theory. Expect...

I listened to a recent episode of Cal Newport's "Deep Questions" podcast, where he interviews Emile P. Torres. Cal says that if you want to understand what is happening in AI, you have to understand the futurist ideologies that shape the people running the frontier labs. Torres is a researcher who studies eschatological and utopian movements. They spent a decade inside this movement as a true believer, published in it, worked as a research assistant to Ray Kurzweil, did a stint at Cambridge's Centre for the Study of Existential Risk, and then defected in 2019. TESCREAL Torres coined " TESCREAL " with the computer scientist Timnit Gebru around late 2022. They were trying to name the seven ideological drivers behind the race to build artificial superintelligence : Transhumanism, Extropianism, Singularitarianism, Cosmism, Rationalism, Effective Altruism, and Longtermism. This is also roughly the chronological order these ideologies emerged over the last 40 yea...

This is the second half of my HPTS 2026 notes. Day 1 was mostly about AI and the importance of specifications . Day 2 and day 3 cover hardware, object storage, failures, consensus, and lakehouses. Session 5: Hardware will save us all (chair: Natassa Ailamaki) The Fastest Way to be the Fastest (Bobbi Yogatama, NVIDIA) GPUs and databases have a love-hate relationship, and Bobbi listed the three reasons: limited GPU memory capacity, the interconnect bottleneck, and engineering complexity. The first two are being fixed by the hardware roadmap. HBM is getting larger and faster. Interconnects and network fabrics are getting faster. But engineering complexity requires some work. No one is eager to rewrite their database to get it work with a GPU. Bobbi introduced Sirius , a GPU-native composable analytics engine. It offers a drop-in accelerator for your existing database, with GPU-native execution underneath. MICE is the design principle: modular, interoperable, composable, extensible. Bobbi ...

Jim Gray started HPTS  42 years ago, and it still runs the same way at Asilomar with 0 proceedings, 1 track, 100 invited people, and ample discussion breaks. It's one of my favorite events, and I look forward to attending it every two years. This is my...umm...fifth HPTS. I have been attending all of them since 2015 , but I seem to have missed it in 2019 . Yep, my life is a blur, even for me. Here are my notes from day 1. I will put day 2 and day 3 in a second post. Keynote: Reality is the Final Verifier. Two Key Gaps in Agentic Software Engineering (Ion Stoica, UC Berkeley) Ion started with the promising parts. LLMs are able to solve difficult math problems, and provide proofs for conjectures that have been outstanding for many decades (Ok, maybe this is not as promising to mathematicians). LLMs also play scientist with AlphaEvolve, and OpenEvolve. In summer 2025 Berkeley ran a seminar where students applied agentic tools to research problems. They took a published state-of-the-a...