That's a great idea. I am +1 as well. Thanks, David
On Tue, Aug 9, 2022 at 11:54 PM Guozhang Wang <wangg...@gmail.com> wrote: > > +1 as well. I think adding such proofs in the repo could encourage more > people reviewing and challenging it, helping to improve whenever we see > fit. Also it helps readers better understand the design patterns. > > One thing worth noting though is how to make sure the proofs are keep up to > date with the actual designs, for large refactoring that touches on related > modules, e.g. the replication protocol etc, I think we should include the > proofs as part of the scope. > > > Guozhang > > On Thu, Jul 28, 2022 at 9:52 AM Matthew Benedict de Detrich > <matthew.dedetr...@aiven.io.invalid> wrote: > > > +1 from me as well, having the formal TLA+ proofs in the main repo is > > hugely beneficial not only from understanding the high level protocol but > > also in terms of awareness/making sure the proof is not outdated. > > > > -- > > Matthew de Detrich > > Aiven Deutschland GmbH > > Immanuelkirchstraße 26, 10405 Berlin > > Amtsgericht Charlottenburg, HRB 209739 B > > > > Geschäftsführer: Oskari Saarenmaa & Hannu Valtonen > > m: +491603708037 > > w: aiven.io e: matthew.dedetr...@aiven.io > > On 26. Jul 2022, 16:58 +0200, Tom Bentley <tbent...@redhat.com>, wrote: > > > Hi, > > > > > > I noticed that TLA+ has featured in the Test Plans of a couple of recent > > > KIPs [1,2]. This is a good thing in my opinion. I'm aware that TLA+ has > > > been used in the past to prove properties of various parts of the Kafka > > > protocol [3,4]. > > > > > > The point I wanted to raise is that I think it would be beneficial to the > > > community if these models could be part of the main Kafka repo. That way > > > there are fewer hurdles to their discoverability and it makes it easier > > for > > > people to compare the implementation with the spec. Spreading familiarity > > > with TLA+ within the community is also a potential side-benefit. > > > > > > I notice that the specs in [4] are MIT-licensed, but according to the > > > Apache 3rd party license policy [5] it should be OK to include. > > > > > > Thoughts? > > > > > > Kind regards, > > > > > > Tom > > > > > > [1]: > > > > > https://cwiki.apache.org/confluence/display/KAFKA/KIP-848%3A+The+Next+Generation+of+the+Consumer+Rebalance+Protocol#KIP848:TheNextGenerationoftheConsumerRebalanceProtocol-TestPlan > > > [2]: > > > > > https://cwiki.apache.org/confluence/display/KAFKA/KIP-853%3A+KRaft+Voter+Changes#KIP853:KRaftVoterChanges-TestPlan > > > [3]: https://github.com/hachikuji/kafka-specification > > > [4]: > > > > > https://github.com/Vanlightly/raft-tlaplus/tree/main/specifications/pull-raft > > > [5]: https://www.apache.org/legal/resolved.html > > > > > -- > -- Guozhang
