4 ms·

In which is revealed the genesis of pron's worldview.

by tome 10y ago

pron 10y ago
If by that you mean that "my" world view is based on some of the most cited publications in computer science (all by Turing Award winners), then yeah. I'm sorry to disappoint, but "my" world view is simply the mainstream world view in the software verification community, as well as in those parts of industry concerned with writing correct software (from what I can gather). I didn't realize anyone thinks there's anything particularly exceptional or controversial about it. I'm sad to say that it's nothing more than the boring mainstream view. It was Robin Milner, John Backus (also Turing award winners) and their spiritual descendants who were (and are) the daring renegades... I just find it important to mention the "classical" POV as some people -- due to whatever circumstances -- seem to believe that "mathematical" CS started with Milner (and then you start hearing strange, incorrect, stuff like "by the Curry-Howard Isomorphism, Turing completeness is isomorphic to logical inconsistency"). I really wish I could count myself a rebel and to follow Milner's vision, but, alas, in my professional life (I hope just there) I'm often a boring old fuck and a (die-hard?) pragmatist, who insists that, as cranky Dijkstra said to the visionary Backus (I'm paraphrasing), "I'll believe it when I see it". What can I say? I think Dijkstra would still be waiting. I am, however, extremely impressed with Rust :) * https://scholar.google.co.il/scholar?cluster=2431409224974074510 https://scholar.google.co.il/scholar?cluster=243140922497407... * https://scholar.google.co.il/scholar?cluster=11090473566849534746 https://scholar.google.co.il/scholar?cluster=110904735668495... * https://scholar.google.co.il/scholar?cluster=13567199892119170764 https://scholar.google.co.il/scholar?cluster=135671998921191... Oh, but things do get interesting when the relationship between languages and "concepts" (i.e. state machines) is formulated as a Galois connection (and then abstract interpretation is born). The paper that I've found most educating on the subject is this: http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.16.4564&rep=rep1&type=pdf http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.16.4... But yeah, I find Lamport extremely convincing (especially as his approach has been demonstrated to work well in industry and to scale to very large production systems) :) --- P.S. A shorter, maybe snarkier, version of this note is here: http://research.microsoft.com/en-us/um/people/lamport/pubs/deroever-festschrift.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/d... ("Computer scientists collectively suffer from what I call the Whorfian syndrome")
- tome 10y ago
  Sorry if you interpreted that as some sort of criticism. That was not my intention. I'm just saying that I can now understand precisely where all your comments about state machines, proving things with simple mathematics, and disdain for languages comes from. By the way, it also makes me cringe when I hear functional programmers talk about how useful Curry-Howard is. On the other hand I don't yet see how state machines can be more useful for my day-to-day work than PFP. I'm trying very hard though ...
  - pron 10y ago
    > I can now understand precisely where all your comments about state machines, proving things with simple mathematics, and disdain for languages comes from. Yep, I've been thoroughly persuaded by that work (not this particular article, which I only came across a couple of weeks ago), and am now a Lamport fanboy! I wouldn't say it's disdain for languages as much as disdain for putting languages front and center (which may -- I won't deny it -- breed a certain disdain for languages that are constantly being put front and center...). > I don't yet see how state machines can be more useful for my day-to-day work than PFP. I'm trying very hard though ... That may depend on what you do. You may find TLA+ or Alloy[1] extremely useful, or maybe you won't. I simply could not possibly write the complex distributed datastore I'm working on without specifying it in TLA+. Theoretically, I guess I could have used Isabelle or maybe even Coq (Vardi), but that would have taken me an order of magnitude longer to learn, and an almost unimaginable effort to actually specify (I'm unaware of such large-scale specifications in Isabelle, let alone in Coq). But my main point is this: the state machine approach isn't necessarily more useful than FP as a form of reasoning about programs (that would depend on the particular program), but it is absolutely far easier (verified by various attempts of trying to get engineers to use TLA+ vs. Coq). I also think it is more fundamental (as FP is defined in terms of state machines, AKA a "computational process", as in http://www.paultaylor.eu/~pt/stable/prot.pdf http://www.paultaylor.eu/~pt/stable/prot.pdf) but not vice versa -- though it could be, with monads! -- but this is mostly a matter of taste. What I care about is ease and simplicity (which often translate to practicality). [1]: Personally, I much prefer TLA+, if only for the elegance, minimalism and sheer power (I think it's the Lisp of mathematical specification of programs). Alloy may be better suited to some tasks, though. Learning TLA+ may make you appreciate how TLA unifies programs with properties about programs into a single concept; in a twisted way you can think of it as programming with types only.

In which is revealed the genesis of pron's worldview.

by tome 10y ago

In which is revealed the genesis of pron's worldview.

pron 10y ago

If by that you mean that "my" world view is based on some of the most cited publications in computer science (all by Turing Award winners), then yeah. I'm sorry to disappoint, but "my" world view is simply the mainstream world view in the software verification community, as well as in those parts of industry concerned with writing correct software (from what I can gather). I didn't realize anyone thinks there's anything particularly exceptional or controversial about it. I'm sad to say that it's nothing more than the boring mainstream view. It was Robin Milner, John Backus (also Turing award winners) and their spiritual descendants who were (and are) the daring renegades... I just find it important to mention the "classical" POV as some people -- due to whatever circumstances -- seem to believe that "mathematical" CS started with Milner (and then you start hearing strange, incorrect, stuff like "by the Curry-Howard Isomorphism, Turing completeness is isomorphic to logical inconsistency"). I really wish I could count myself a rebel and to follow Milner's vision, but, alas, in my professional life (I hope just there) I'm often a boring old fuck and a (die-hard?) pragmatist, who insists that, as cranky Dijkstra said to the visionary Backus (I'm paraphrasing), "I'll believe it when I see it". What can I say? I think Dijkstra would still be waiting. I am, however, extremely impressed with Rust :) * https://scholar.google.co.il/scholar?cluster=2431409224974074510 https://scholar.google.co.il/scholar?cluster=243140922497407... * https://scholar.google.co.il/scholar?cluster=11090473566849534746 https://scholar.google.co.il/scholar?cluster=110904735668495... * https://scholar.google.co.il/scholar?cluster=13567199892119170764 https://scholar.google.co.il/scholar?cluster=135671998921191... Oh, but things do get interesting when the relationship between languages and "concepts" (i.e. state machines) is formulated as a Galois connection (and then abstract interpretation is born). The paper that I've found most educating on the subject is this: http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.16.4564&rep=rep1&type=pdf http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.16.4... But yeah, I find Lamport extremely convincing (especially as his approach has been demonstrated to work well in industry and to scale to very large production systems) :) --- P.S. A shorter, maybe snarkier, version of this note is here: http://research.microsoft.com/en-us/um/people/lamport/pubs/deroever-festschrift.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/d... ("Computer scientists collectively suffer from what I call the Whorfian syndrome")

tome 10y ago
Sorry if you interpreted that as some sort of criticism. That was not my intention. I'm just saying that I can now understand precisely where all your comments about state machines, proving things with simple mathematics, and disdain for languages comes from. By the way, it also makes me cringe when I hear functional programmers talk about how useful Curry-Howard is. On the other hand I don't yet see how state machines can be more useful for my day-to-day work than PFP. I'm trying very hard though ...
- pron 10y ago
  > I can now understand precisely where all your comments about state machines, proving things with simple mathematics, and disdain for languages comes from. Yep, I've been thoroughly persuaded by that work (not this particular article, which I only came across a couple of weeks ago), and am now a Lamport fanboy! I wouldn't say it's disdain for languages as much as disdain for putting languages front and center (which may -- I won't deny it -- breed a certain disdain for languages that are constantly being put front and center...). > I don't yet see how state machines can be more useful for my day-to-day work than PFP. I'm trying very hard though ... That may depend on what you do. You may find TLA+ or Alloy[1] extremely useful, or maybe you won't. I simply could not possibly write the complex distributed datastore I'm working on without specifying it in TLA+. Theoretically, I guess I could have used Isabelle or maybe even Coq (Vardi), but that would have taken me an order of magnitude longer to learn, and an almost unimaginable effort to actually specify (I'm unaware of such large-scale specifications in Isabelle, let alone in Coq). But my main point is this: the state machine approach isn't necessarily more useful than FP as a form of reasoning about programs (that would depend on the particular program), but it is absolutely far easier (verified by various attempts of trying to get engineers to use TLA+ vs. Coq). I also think it is more fundamental (as FP is defined in terms of state machines, AKA a "computational process", as in http://www.paultaylor.eu/~pt/stable/prot.pdf http://www.paultaylor.eu/~pt/stable/prot.pdf) but not vice versa -- though it could be, with monads! -- but this is mostly a matter of taste. What I care about is ease and simplicity (which often translate to practicality). [1]: Personally, I much prefer TLA+, if only for the elegance, minimalism and sheer power (I think it's the Lisp of mathematical specification of programs). Alloy may be better suited to some tasks, though. Learning TLA+ may make you appreciate how TLA unifies programs with properties about programs into a single concept; in a twisted way you can think of it as programming with types only.