5 ms·
this is how you end up with darcs as your version control system. It’s provably correct, but about 1 in 10 times it hangs forever and never terminates. Also it
by jes5199 8y ago
this is how you end up with darcs as your version control system. It’s provably correct, but about 1 in 10 times it hangs forever and never terminates. Also it doesn’t implement branching because that’s out of scope for the model.
- viraptor 8y agoI think you're mixing the result of implementation and the way something's implemented. Darcs relies on abstract theory which implemented didn't end up very performant or full of features. But it would be close to the same speed if it was implemented in terrible C. On the other hand you can write provable implementation of git with similar speed as the current one.
- nickpsecurity 8y agoNah, it's how you end up with HACL*: verified crypto that performs like C shipping in Firefox. https://github.com/project-everest/hacl-star https://github.com/project-everest/hacl-star You can verify stupid designs or smart ones. You can do impractical verification or pragmatic approaches. Formal verification is a tool whose outcomes depend on who wields it. The only consistent drawbacks it has are requiring more expertise, the project takes longer, and the project has to be simplified in design/implementation. High-quality software in general (eg OpenBSD) often has same properties, though. Possibly intrinsic to achieving correctness rather than additional requirement of formal methods.