Is it possible to build something like "consensus type" based on tyrade?

[zhiqiangxu]

We know consensus(pbft, raft, paxos etc) is a big topic for distributed systems, which are hard to verify.

There's some tools like tla or coq, which can help verify simple systems, but neither verifies rigorously, or are too complex to do it rigorously.

Can tyrade help in this case?

What application areas can benefit from a type-level programming language? Session types are the most complex example I've seen so far, but I'd be really interested to find other use cases for Tyrade.

This is also a reply to the question.

[willcrichton]

That's a great question! From what I know about verifying consensus protocols, that seems like a challenging kind of proof to embed in a type system. My understanding is that those proofs usually have the form:

• write an imperative program in a while (true) {} loop that does a bunch of communication
• write an inductive invariant that specifies what should be true across each loop iteration
• use an SMT solver or something to prove that a high-level property is true given the inductive invariant

(At least, I read the paper "Ivy: safety verification by interactive generalization" and that was my impression. )

So if we wanted a complex proof about consensus in e.g. Tyrade, we would either need something like Coq-style proof tactics or an SMT solver to do the heavy lifting of proof search.

[zhiqiangxu]

I tried Coq several years ago, the impression is it's too verbose, not fit for complex proofs.

I also tried tla, the impression is that the proof is not exact, one has to minimize the number of states, and the temporal logic stuff of safeness and liveness is hard to grasp, easy to forget:(

Not sure if Tyrade can fit in the middle ground !