18 ms·
Care to elaborate? Perhaps the tools to do this in practice aren't there (which just shows how young the field of software "engineering" really is), but what co
by DrSusanCalvin 10mo ago
Care to elaborate? Perhaps the tools to do this in practice aren't there (which just shows how young the field of software "engineering" really is), but what consensus are you talking about and how is it an obstacle to verifying code? Most of the web follows standards and protocols, which actually sort of a prerequisite for communications across different systems...
- engineeringwoke 10mo agoBasically the modern web uses orchestration, for pretty much everything. Usually Kubernetes is doing that. Theoretically protocols like RAFT are formally verifiable, but their implementations in orchestration tools like etcd have not been, and I would go so far as to say that that is an impossible task. Therefore, the entire exercise is kind of silly.
- DrSusanCalvin 10mo agoThanks, interesting. However, that just seems like a protocol like any other, with no real reason why you "can't" formally verify it. Is there something special about a consensus algorithm / protocol that makes it any more difficult to verify than any other algorithm which doesn't yet have a formally verified implementation? Edit: https://link.springer.com/chapter/10.1007/978-3-319-48989-6_8 https://link.springer.com/chapter/10.1007/978-3-319-48989-6_...
- engineeringwoke 10mo agoThat would be like saying that you can verify the software that CERN uses to measure the Higgs Boson because we verified general relativity.
- DrSusanCalvin 10mo ago> You can't formally verify anything that uses consensus What did you mean by this then? There certainly seems to be nothing special about consensus that makes it any harder to verify than anything else. It's not fundamentally impossible to verify the software that CERN uses, it just takes some work.