Viewing profile — oggy

I'm not a mathematician either ;) Yeah, I won't sit around and ponder at a property definition for weeks. But I will maybe spend a day on it, not get anywhere, and then spend an ho…

In my experience, finding the "correct" specification for a problem is usually very difficult for realistic systems. Generally it's unlikely that you'll be able to specify ALL the …

I see, so it unifies type (or I suppose term in this case?) erasure and linear typing? Thanks for the explanation!

I haven't followed closely, and I'm only faintly acquainted with algebraic geometry and category theory. But the TFA links to a formalization of Grothendieck schemes, which are def…

Thank you for spelling this out; comments like these make this website worthwhile. You've enlightened at least one person today. You hinted that there's more to QTT (or its impleme…

Thank you for the kind words! I haven't really talked about it anywhere yet since it's fresh off the press, I'll definitely post it on the mailing list.

I think the main answer was given by another comment: for most projects, correctness usually isn't worth that much (i.e., a bug isn't that expensive for a company producing a piece…

Funny to see this posted on HN, just last week I finished writing a blog post about a project I did for checking that code matches the TLA+ specs so I have to shamelessly plug it :…

A funny anecdote from a concert a few years ago: Allen was playing a solo, holding a note and blowing as hard as he could on his little soprano sax. Next thing you his teeth fly ou…

Maybe not range per se, but there are a couple of Europe-specific things that make EVs less attractive. First, many people live in apartment buildings and park their cars on the st…

TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for …

"Verifying" and "proving" are synonymous in this case. You prove or verify that the system satisfies some specification, i.e., properties. Your normally write the properties yourse…

Great to see this. I hope it takes off - Bazel is useful but I really like the principled approach behind it (see the Build Systems a la Carte paper), and Neil is scarily good from…

FWIW, I have a PhD in formal methods and spent a good chunk of that PhD proving stuff about distributed systems in Isabelle. I'm vaguely familiar with Coq. At work I've been largel…

Thanks for your work, Hilel! I've been using TLA extensively in my job the last few months (I work at a blockchain company), and it's been a good run - we found a bunch of issues i…

I used Spin a few years back, so my memory is a bit hazy, but I remember Promela (Spin's modeling language) feeling extremely low-level in comparison. It felt a bit like more limit…

I bought a Remarkable 2 for note taking and annotating scientific papers. As far as it's promise of "better paper", I think it's only partly fulfilled. I haven't returned it, but I…

The idea is not to replace every banking system, but to create a network with a sufficient technological edge over existing solution and sufficient business value. CHESS is definit…

I don't have a financial services background myself, so assessing I can't really comment on the risk of consolidating custodianship and trading. But market consolidation will at so…

Shameless plug: the problems that you describe are almost exactly what we're trying to solve with DAML and Canton [1]. From the Canton whitepaper: Building distributed applications…

AI can be very useful in practice for theorem proving WITHOUT proving "big new theorems" or inventing new mathematics. Right now, what makes theorem proving an extremely expensive …

Sorbillo's is the best I've tried. I remember walking in front of the shop a few times and thinking it's some kind of tourist trap (it's on the possibly most touristy street in the…

Yeah, like I said I don't know what the current available supply is, which IIUC is the more limiting factor. I also don't know what the current prices are, and I don't know which p…

Before the outbreak, N-95 masks used to cost 58 cents. So if it was spent on masks only, around 1.7 million masks at those prices. I don't know how many health workers SF has, but …

I've attended several short courses on giving presentations. This one by an ETH Zurich professor is the best one I know of: https://inf.ethz.ch/personal/markusp/teaching/guides/gui…