3 ms·
Excellent quotation in the intro to that paper: > ... Our intention is not to use any deep theorems of category theory, but merely to employ the basic concepts
by mbrock 11y ago
Excellent quotation in the intro to that paper:
> ... Our intention is not to use any deep theorems of category theory, but merely to employ the basic concepts of this field as organizing principles. This might appear as a desire to be concise at the expense of being esoteric. But in designing a programming language, the central problem is to organize a variety of concepts in a way which exhibits uniformity and generality. Substantial leverage can be gained in attacking this problem if these concepts are defined concisely within a framework which has already proven its ability to impose uniformity and generality upon a wide variety of mathematics.
(John Reynolds, "Using category theory to design implicit conversions and generic operators", 1980.)
- deleted 11y ago[deleted]
- omginternets 11y agoI'm truly glad that you're enjoying that paper :) This is completely unrelated, but I found this paper to be similarly brilliant in its simplicity, clarity, and rigorous explanation: https://ramcloud.stanford.edu/raft.pdf https://ramcloud.stanford.edu/raft.pdf
- zeckalpha 11y agoThat paper took 25 years to refine. Additionally, for the right audience, more math could make it more succinct.
- omginternets 11y agoI don't doubt it, but I'm not sure what you're trying to say. Would you elaborate?
- catnaroek 11y agoI have a hard time already convincing myself that correct sequential imperative algorithms are indeed correct - which probably means that I'm a bad programmer, but I can't change who I am. So convincing myself that that Raft, a concurrent algorithm, is correct (meets its specification) from an informal description is completely out of question - where is the formal proof of correctness?
- mbrock 11y agoTake a look here for pointers to formal proofs: https://news.ycombinator.com/item?id=10017549 https://news.ycombinator.com/item?id=10017549 Specifically Verdi, a Coq framework for distributed system verification, which now includes a formally proven Raft implementation. https://github.com/uwplse/verdi https://github.com/uwplse/verdi This appears to be the main theorem, "raft_linearizable": https://github.com/uwplse/verdi/blob/master/raft-proofs/EndToEndLinearizability.v https://github.com/uwplse/verdi/blob/master/raft-proofs/EndT...
- catnaroek 11y agoThank you very much. :-)
- omginternets 11y agoAh, sorry. I think you're reading this with a much deeper understanding of mathematics than I. I'm really curious, though. Could you give me some insight into how algorithms are proven correct?
- deleted 11y ago[deleted]