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 hour or two a day thinking about ways to formulate it. Sometimes I try something, then an hour later figure out it won't work, but sometimes I really do just stare at the ceiling with no idea how to proceed. Helps if you have someone to talk to about it!

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 relevant properties formally. I think there's probably some facet of Kolmogorov complexity there; some properties probably cannot be significantly "compressed" in a way where the specification is significantly shorter and clearer than the solution.

But it's still usually possible to distill a few crucial properties that can be specified in an "obviously correct" manner. It takes A LOT of work (sometimes I'd be stuck for a couple of weeks trying to formalize a property). But in my experience the trade off can be worth it. One obvious benefit is that bugs can be pricey, depending on the system. But another benefit is that, even without formal verification, having a few clear properties can make it much easier to write a correct system, but crucially also make it easier to maintain the system as time goes by.

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 definitely post-WW2 material, and they rely on the Isabelle's locales feature. Are you familiar with this work? How far from the "ordinary mathematician's style" is it?

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 implementation in Idris?) than this. Could you elaborate a bit on what these other features are, and what their purpose is?

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 of software). It also isn't in the software culture (yet?). Today people will be shocked if you don't have a version control system and a CI pipeline. Few people had one 20 years ago. Also, people are often reluctant to learn a new paradigm (think functional programming).

Having done multiple TLA verification projects myself, here are some technical ones:

1. It's actually surprisingly hard to write a good specification, i.e., precisely and formally state what you want. Often it's not even practical, i.e., the specification is so complex that you end up nearly recreating the implementation. Kolmogorov complexity is also a thing for specifications, I suppose ;) 2. TLA in particular is mostly useful for concurrent/distributed systems. 3. Model checking (the method used to verify the TLA models) hits limits pretty quickly. E.g., you may be able only check your system for 2 threads, but forget about 3 threads. 4. The TLA tooling is very clunky by modern standards.

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 :) [1] I was aware of the MongoDB paper, but I ended up actually doing exactly what they suggested wouldn't work: I instrumented Rust programs to log traces and checked them against the specification. Even though the models were largely also post-factum models as in their case (i.e., the code was there first, and models were built later on), this worked for us since the models really were aimed at capturing the implementation's behavior. Our target implementation is possibly smaller than what they had to deal with, though (it's only around 5kLoC of Rust smart contracts) so that's a factor.

My technique was slightly different, though. First, I ended up ignoring the initial states, because tests would often manually create fixtures that would serve as a starting point. So I only ended up checking that trace steps obey the transition predicate, which is weaker, but hey, all this is best-effort only anyways. Second, I ended up using the Apalache tool instead of TLC; the reason being that my transitions were sometimes of the form "there exists a number between 1 and N". While model checking you would pick a small N, but in the test runs where the traces come from the N was sometimes huge. TLC ends up enumerating all the possibilities between 1 and N, whereas Apalache translates the whole thing into an SMT formula which is generally trivial to check. Apalache also has the side benefit of requiring type annotations (and providing a type checker) which makes the models a lot easier to refactor when the code changes.

I also ended up creating a small library for helping instrument Rust programs to collect such logs. The idea here was to minimize the amount of logging statements in the production code, to keep it out of the way of the people working on the code base who aren't familiar with TLA. It's somewhat specific to our code base, and there's a fair amount of unsafe nastiness that works only because our code is of certain shape, but in case someone's interested, it's open source: https://github.com/dfinity/ic/tree/master/rs/tla_instrumenta....

I wasn't aware of the 2024 paper they reference though, so curious to see what approach they took.

[1] https://www.mongodb.com/blog/post/engineering/conformance-ch...

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 out, and there's a general commotion on as the rest of the band goes searching for the denture on the stage.

Amazing to be alive at that age, to be touring and rocking it, that's another level.

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 street, with no charging facilities. So they'd have to make that supercharger trip pretty often. Second, on any given Saturday in July and August there will be millions of people driving for vacation (1000+ km not being uncommon), mostly to the Mediterranean or back to their country of origin (Eastern Europe, Balkans, Turkey). In this period I've already ended up queuing for 10-15 minutes for gas - I can imagine it would be worse without chargers. Also, people who take their car to the poorer European countries often do it because of poor public transport infrastructure there, so the likely poorer EV infrastructure there would play somewhat of a role as well (though likely minor).

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 Apalache) and your desired properties into an SMT formula, and you let the solver have a go at it. The deal is that the SMT language is quite expressive, which makes such encodings... not easy, but not impossible. And after you're done with it, you can leverage all the existing solvers that people have built.

While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done.

[1]: https://apalache.informal.systems

"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 yourself, but sometimes the properties are hardcoded (e.g., your code doesn't panic).

You don't need a particularly strong formal background in CS or maths to verify code, but it's a challenging task never the less.

1. The first challenge where people often give up is that you will often need to reason about your code in a different language than the code itself (not necessarily true for Verus that's being discussed here). In that sense it helps a lot if you already know multiple programming languages, ideally using different paradigms. 2. The second challenge is that you will need to be actually precise in describing what your want your program to. This is a lot harder than it sounds; there's no hand-waving, no "works in practice", but even beyond that, it's actually really difficult to express what you want from the program succinctly, and often not even possible or feasible. On the other hand, this is possibly the most practical skill you will currently be able to take away from the verification tools; it absolutely can change the way how you work, how you collect requirements, and how you go about writing code. 3. The third challenge is then actually performing the verification/proofs. This is currently painfully hard; most literature I've seen comes up with a ration between 5-20x between the amount of code you're verifying (in terms of lines of code, say) and the number of "proof lines" you need to write in some form. This may make sense for extremely critical code where a bug can cost tons of money; e.g., aerospace, or huge companies with tons of users - AWS is doing proofs at a fairly large scale, Apple is now doing the same at a smaller scale too. I would generally recommend NOT writing proofs if you can, but using tools that can do some kind of limited or heuristic verification. Which tools exactly I would recommend for a "working programmer" depend on what you're trying to do. For example, if you are writing concurrent or distributed code, I would recommend using something like TLA and the associated TLC tool. For lower-level Rust code (data structures and similar), I'd recommend the Kani verifier over something like Verus. For many other languages, the choices are limited or non-existent.

Zero-knowledge proofs roughly allow you to convince someone that something is true, without leaving them any wiser WHY it's true. Generally this is not what's interesting for software verification, but it's nevertheless extremely cool (because it's super counterintuitive). Most of the excitement indeed comes from blockchains, where these things are used, but it's debatable whether they're really practical. You can use them to transfer crypto around already today, without revealing the identities of the sender or recipient for example. However they are still computationally quite expensive and only work because there's currently not so much volume in crypto.

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 my experience of working with him so I'd expect that they've come up with something awesome.

One thing I find annoying with all of these general, language-agnostic build systems though is that they break the "citizenship" in the corresponding language. So while you can usually relatively easily build a Rust project that uses crates.io dependencies, or a Python project with PyPi dependencies, it seems hard to make a library built using Bazel/Buck available to non-Bazel/Buck users (i.e., build something available on crates.io or PyPi). Does anyone know of any tools or approaches that can help with that?

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 largely using TLA+ the last few months to analyze designs of distributed protocols.

What I'll say is a simplification, but I'd describe TLA+ as a one-trick pony, that does that one trick very well. Roughly, you have to structure the model of your algorithm as a transition system, described using a predicate on "these are the legal initial states", and another predicate over two states that says how you can move from one state to the next. To describe these predicates, you get a fairly simple but expressive language at your disposal (a TLA cheat sheet probably fits a single page). This format lends itself well to describing high-level ideas of distributed protocols or concurrent algorithms (roughly what you'd write as pseudocode for those protocols/algorithms). You can then use that same predicate language, plus some additional operators to talk about time (e.g., you can say things like "never" or "eventually"), to specify what your system should do. Finally, you get an automated analysis tool (actually two tools these days, TLC and Apalache), that checks whether your model satisfies the specification. The beauty is that the checking is push-button - after you've finished writing the model and the spec, your work is largely complete. The analysis will have severe limitations; your model can't be too big, and it has to be finite (e.g., if you're writing a model of a distributed protocol, you have to limit the analysis to settings with a handful of nodes), but in practice even this limited analysis weeds out most of the bugs.

Isabelle and Coq are theorem provers (there's also a bunch of other theorem provers). That means, you have to define whatever you're modeling as a mathematical object, and then you go off and prove stuff about it. They're both extremely flexible - you can model a transition system just like TLA does, but you can also talk about any kind of mathematics (algebra, statistics, financial math, whatever). You can also encode programming language semantics, as well as program logics, that allow you both model actual C or OCaml or whatever code, and to specify properties about programs (as mathematical theorems) and prove them in a more comfortable way using program logics. The analysis (which corresponds to proving a theorem) is generally not limited (e.g., you prove a distributed protocol correct for any number of nodes).

The snag is that in Isabelle or Coq the proof is done in a largely manual way (you have to sort of type in the argument by hand, often in excruciating detail). If you want to verify a program with N lines of code, you'll typically end up writing 5-20 times N lines of proof to convince the theorem prover of the correctness of the said program. But to do this, you'll generally have a large library of already proved theorems (6-7 years ago I counted around 200k theorems available for Isabelle), and you will generally have a "metaprogramming language" at your disposal to write your own analysis (i.e., proof) procedures.

For academics, especially programming languages and formal methods people, their work is often writing new programming logics, or new proving procedures, or developing whole new theories. Theorem provers lend themselves better for that kind of work, as well as pushing boundaries, such as doing code-level analysis. But for engineering, TLA can be the 80/20 solution in many cases.

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 in several designs and even implemented code (some fairly critical). My secret hope is to get some co-workers to start using TLA themselves (so I can go off to do code-level verification instead hehe), I've organized a couple of internal tutorials but no takers so far - hopefully this free learning resource will help advance that goal :)

On a related topic, does anyone know of a comparison to Alloy 6? I've been meaning to take a day or two to look at it (I tried Alloy out a while ago while I was still in my PhD, but have forgotten most of it), I'm curious to see how it stacks up.

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 limited C with non-deterministic choice stuck in there. TLA is a first-order logic language, and the tooling (while not great by modern language standards) felt more pleasant than Spin.

It could be that you get faster model checking with Spin though, I'm not aware of any comparisons.

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'm sadly also not using it regularly.

It's obviously better than paper since you don't end up with stacks of printed articles. The feel of reading and writing is also exactly like paper, which is great. You get some basic select/cut/paste functionality, which improves on paper. But.

I used it to take notes at work, create simple TODO lists etc. The issue with this is that the resulting notes are way harder to navigate than a simple paper notebook, as the software doesn't support even basic bookmarks. Whereas with paper I can add bookmarks as I please, a paper organizer notebook allows me to navigate my calendar easily etc. I'm still amazed that the RM software offers absolutely no functionality for such navigation. This is a huge drawback for me.

When using it to annotate PDFs, the app offers you a few tools (pencil, pen, eraser, etc). Ideally you'd like to fit the article on the remaining portion of the screen, possibly cropping the margins if your the article is created for a different page size and your eyesight is as bad as mine. But the support for this sucks, as the toolbox always covers a piece of the document, so you end up having to hide/unhide it constantly.

Next, while the pen feels quite good, and feels almost as precise as a real pencil, I find the eraser quite hard to control. It erases an area somewhere around the end of the pen, but unlike a physical eraser, you don't see its boundaries. There's no support for stroke-based erasing. Finally, stating the obvious, the device is black-and-white. But I find different colors helpful when annotating papers, or creating sketches of systems etc.

So right now I can't really recommend the device, but I'm still holding onto mine hoping it will improve. I think the hardware can serve as a basis for better paper - but I think the software would need many of the features of http://www.styluslabs.com/ to get there

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 definitely a complex beast. The go-live date has moved from 2021 to 2023, AFAIK at the request of the participants. To your question when it will be directly (as in, through DAML) used by all participants - I guess at the point where it generates enough value that it's advantageous for them to use it.

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 some point run into legal and jurisdictional limits (data sovereignty), if not other ones first (do I really trust that giving you all this data doesn't give you an edge?). The idea behind the virtual shared DB is that you don't have to outsource the data, but you can still transact (with strong consistency) over data shared with many entities.

Like I said, I don't have a background in financial services myself, but there are people on my team who have vowed to never have to do reconciliation again. As you seem to wear the same scars, I'm very curious to hear your thoughts on the whitepaper based on your other good comments in the thread. Feel free to e-mail me (address in profile) or post here.

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 that involve multiple organizations is hard with today’s technology. For each application, all organizations must agree on the data encoding, transport mechanisms, and interaction rules, and all must implement their part of the interaction correctly, including authentication and authorization. Once implemented, such an application often becomes a silo: there is no general convenient, secure and privacy-preserving way to integrate such applications and compose the business workflows that they automate.

The big problem is bootstrapping the network; as you say, setting up yet another format (DAML in this case) is a huge ask. But we're starting to see the beginnings of a network, as in the next couple of years the Australian [2] and north-bound (i.e., mainland China) Hong Kong securities [3] will be accessible through DAML.

[1]: https://canton.io [2]: https://www2.asx.com.au/markets/clearing-and-settlement-serv... [3]: https://www.ledgerinsights.com/hkex-daml-smart-contract-stoc...

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 undertaking is making proof search work. AI could help immensely by improving the search.

The process of proving things in provers like Lean, HOL or Coq is interactive; roughly, the theorem you want to prove is your starting goal, and you apply tactics to transform the proof goal until the goal becomes the boolean value true. The Platonic ideal of this process is that you provide the main, "creative" steps of the goal transformation, and the tactics discharge the rest automatically. In practice, however, for the process to work, you need to carefully state your theorems in a certain way, and you need an enormous amount of tacit knowledge about how the internals of the tactics, as well as of the libraries of already proved facts that you can use. These things take years of practice to build up. I think it unlikely that theorem provers will see a significant uptake until the tactics (i.e., proof search) improve massively.

This is where I hope AI could step in. There are many challenges, obviously. The training data sets are relatively modest; when I looked a few years ago, the publicly available Isabelle theories, for example, amounted to a few hundred thousand proved theorems, which is a minuscule corpus compared to what something like GPT-3 uses. Then, how do you represent the input, just characters, or do you need more structure? Can you can leverage something like reinforcement learning? How do you could set the training process up? On the other hand, compared to chat bots, the quality of the resulting AI system would be much easier to quantify (success rate on a benchmark of new theorems).

There's already work in this area, but I'm not aware of any grand successes yet. I hope to see much more work on this in the near future. I've been dabbling in it myself a while ago while I was still in academia, but other priorities have taken precedence in the past couple of years.

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 city), but decided to try it out in the end. Absolutely fantastic. The pie was great, but TBH I think there were other places in town whose pies were as good, but the quality of the toppings... just wow. And I was surprised that the price was the same as any other place in town (I think a marinara was something like 3-4 Euros).

My second favorite is in Switzerland of all places, in the small town of Meilen. Amazing toppings too. But I went there once since the start of the lockdowns, and it didn't taste as good. I don't know if it's the pandemic leaving a bitter taste, or just an issue for their supply chains...

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 part of it are production costs and which part is just profiteering.

And even if it's hundreds of masks per worker, I'm sure it won't last through this thing.

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 at a population of 800k and a US average of 2.6 physicians per 1000 people I'd guess it's hundreds of masks per worker.

I don't know about the costs or the currently available supply though, or what the real price increases should be due to a pinched supply chain, and I haven't been able to find any data - would appreciate pointers.

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/guide-p...

He has a list of useful books at the end (I haven't read any of them, though)

Great comment about missing the forest from the trees. The course outline reminds me of an article on "writing great code" that lists the rules of a code formatter.

My personal tips for writing docs: 1. think about what you need to get across and to whom. I've found this categorization helpful (just don't get religious about it): https://www.writethedocs.org/videos/eu/2017/the-four-kinds-o... 2. try to say whatever you're saying with as few words as possible. "Vigorous writing is concise" is probably the best takeaway I got from Strunk & White (not a huge fan of the book otherwise) 3. do a few passes. "Keep rewriting" is probably the best takeaway I got from "On Writing Well" (but I like that book in general).

Your dismissive tone is uncalled for and not appreciated. Here's a systematic review that cites several studies that find face masks show a statistically significant effect in protection against influenza:

https://www.bmj.com/content/339/bmj.b3675.short

If your collaborators can point you to peer-reviewed studies that rebut these results, or to a serious current analysis that shows the impossibility (or estimates the price and time frame) of ramping up PPE production, please post it.

Feedback on the website: it's running quite slow for me on Chromium under Linux, especially if there are a lot of locations (for example, unchecking "exclude public health agencies" makes the site very unresponsive). Also, "exclude local public health agencies" is confusing; I'd expect selecting it to show only those that aren't local public health agencies, but it seems to have the opposite effect. Finally, if I click on one of the locations, what I assume to be X-marks are displayed as just rectangles (I guess a missing Unicode symbol in the font on my machine).

Thanks again for making this!

Thank you for the work on this.

I have a tangentially related question, hoping that someone knowledgeable can answer. What are the main bottlenecks to scaling testing, in particular in the following stages:

- the supply of virus-specific reagents (primers, perhaps virus-specific reporting probes - are these necessary, or can just generic reporters be used?)

- the supply of other reagents (in case of PCR, polymerase, nucleotide material, buffer)

- the supply of disposable testing equipment. I know that swabs are in short supply for some reason, anything else?

- safety in handling both the samples and the amplified product (can you basically flush the processed sample down the toilet, or do you need to handle it with extreme precautions)

Interesting, this is the first time I hear that touching fomites is the primary vector of spreading. The CDC page says the opposite: https://www.cdc.gov/coronavirus/2019-ncov/prepare/transmissi... But I do appreciate that we still have a lot to learn about the virus, so disinfecting your hands frequently and being careful about what you touch is sound advice.

The other benefit of masks (and probably the main one of DIY masks) would be that it decreases the chance of the wearer infecting others.