Lindsey Kuper on Nostr: ✨ Happens-before as a dependent type ✨ In Lamport’s traditional formulation of ...
✨ Happens-before as a dependent type ✨
In Lamport’s traditional formulation of happens-before, the question “Does event A happen before event B?” just has a boolean answer: yes or no, and evidence of that answer exists separately. In our setting, you can't talk about a happens-before relationship without also talking about the causal path that witnesses the relationship. The answer to the question is either "no" or "yes, and here's why!"
In Lamport’s traditional formulation of happens-before, the question “Does event A happen before event B?” just has a boolean answer: yes or no, and evidence of that answer exists separately. In our setting, you can't talk about a happens-before relationship without also talking about the causal path that witnesses the relationship. The answer to the question is either "no" or "yes, and here's why!"