Hooray! We just got word that "Verified Causal Broadcast with Liquid Haskell" (https://arxiv.org/abs/2206.14767), led by my student @redmp, was accepted at IFL '22. (The date is in the past because IFL has a post-conference review process. They're weird like that!)
Short thread about this paper 👇
Causal broadcast is a widely used building block of distributed systems in which participants communicate by exchanging messages. If implemented correctly, it prevents many confusing situations, like this one:
In this paper, we show how causal message delivery can be expressed *as a refinement type*. This means that the Liquid Haskell type checker -- with human assistance -- can tell us that our implementation of causal broadcast will never deliver messages in an order that violates causal delivery!
By "with human assistance", I mean that although Liquid Haskell automates some stuff for you, we (and by "we", I mean @redmp) also had to do a lot of proving by hand to carry out this project. Liquid Haskell is quite possibly the world's weirdest proof assistant, but, amazingly, it actually *is* a proof assistant, which makes this kind of thing possible.
Also, this project is just the first step in what I intend to be a multi-year research agenda that applies refinement types to distributed systems, as described here: https://decomposition.al/blog/2022/01/31/career-building-reliable-distributed-systems-with-refinement-types/
By the way, I'm not in a big rush to hire, but I am casually looking for another Ph.D. student who's specifically interested in working on this (refinement types + distributed systems). If that could be you, let's talk!
@lindsey had a workshop paper “Proof-Carrying Smart Contracts” with @maurice and @vsaraph (+2 more coauthors not on Mastodon as far as I know) that we didn’t end up resubmitting for a full conference because the reviewers wanted a proof of concept implementation and none of us had time to do it, but my idea was to do the POC implementation as higher-order functions in LiquidHaskell.
@elfprince13 @maurice @vsaraph Cool -- last summer @redmp and I were talking with a student at Edinburgh who was interested in using LH for verifying smart contract properties. Not sure if they continued pursuing the idea, but if you're interested, I could put you in touch by email.
@elfprince13 OK, just sent an email introducing you (to thomas@geopi.pe; hope that's correct) to the student! I'll let you decide if you want to loop co-authors or whoever in :)
@lindsey thanks! :)
@elfprince13 @lindsey @maurice I’d forgotten about this work! For convenience looks like the paper is here on Paul’s website https://paulgazzillo.com/papers/wtsc18.pdf
@maurice @vsaraph @lindsey takes the “distributed systems + refinement types” concept in a completely orthogonal direction to what you’re doing here, but just throwing that out in the world because I’d love to see someone run with it one day.