4 ms·

Who computer scientists of today could, in your opinion, be considered Dijkstra's spiritual successors?

wooptoo 5y ago
D.J. Bernstein maybe?
iamcurious 5y ago
There is mathmeth.com, also Ralph-Johan Back, also to some extent me (search for "foundations for mathematical methodology").
bordercases 5y ago
The key insight of Dijkstra is that we should use a kind of substitution calculus to derive programs from invariants. From Dijkstra's time we've seen partial adoptions and spinoffs from these insights. Using lambda calculus and static types gets you program behavior that looks a lot like refinement calculus and invariants (since types label domains that are equivalent to predicate sets, and lambda calculus computation is the substitution model). For that reason I would say that the spiritual successor's to Dijsktra are in the functional programming community, particularly Haskell and Scala: Erik Meijer, Richard Bird, Martin Sapolsky, etc. Carnegie Mellon's Computer Science curriculum is also fairly integrated across the board to use this style of programming and mathematics.
- User23 5y ago
  > The key insight of Dijkstra is that we should use a kind of substitution calculus to derive programs from invariants. It baffles me that the "formal methods" (it really should be called automated methods) crowd not only ignores this lesson, but is completely blind to it. In my direct experience, the ones I've spoken to are so obsessed with verification that the idea of constructing a program that has specified properties apparently isn't even thinkable for them. Perhaps it's a defect in my ability to explain things, but I've never once managed to explain to one of them that construction is a significantly easier task than verification. It's a real shame because they're very intelligent people that I'm certain could contribute greatly to formal program derivation. I suppose it's one of those "professional deformations" Dijkstra occasionally mentions. One of the things I'd like to do when I have copious free time is build an Emacs mode that only allows edits that preserve the given invariants, perhaps using TLA+ or something similar. Anyone that wants to learn more on the subject of deriving programs should read one or both of A Discipline of Programming[1] and Predicate Calculus and Program Semantics[2]. The former is more approachable for the programmer who isn't as inclined toward formal mathematics. The latter basically takes the same concepts and treats them with much greater mathematical rigor. [1] https://www.goodreads.com/book/show/2276288.A_Discipline_of_Programming https://www.goodreads.com/book/show/2276288.A_Discipline_of_... [2] https://www.goodreads.com/book/show/3144463-predicate-calculus-and-program-semantics https://www.goodreads.com/book/show/3144463-predicate-calcul...
  - rramadass 5y ago
    >Anyone that wants to learn more on the subject of deriving programs should read Two more; * EWD316 - A Short Introduction to the Art of Programming. * A Method of Programming - Book co-authored with W.H.J.Feijen. For some reason, this is not well known though it was written as a course textbook. Draft version here: https://www.softwareresearch.net/fileadmin/src/docs/teaching/WS08/SE/A_Method_of_Programming_1.pdf https://www.softwareresearch.net/fileadmin/src/docs/teaching...
- rramadass 5y ago
  Great insight! His idea of the "Weakest Precondition Calculus" is Functional in contrast to "Hoare Triples" which are Relational.
User23 5y ago
Leslie Lamport immediately comes to mind. His work extending predicate transformers for concurrency[1] is a good example. Edit: Tony Hoare isn't a successor, but he's a living genius who shares many of Dijkstra's inclinations. [1] https://lamport.azurewebsites.net/pubs/lamport-win.pdf https://lamport.azurewebsites.net/pubs/lamport-win.pdf

D.J. Bernstein maybe?

There is mathmeth.com, also Ralph-Johan Back, also to some extent me (search for "foundations for mathematical methodology").

bordercases 5y ago

The key insight of Dijkstra is that we should use a kind of substitution calculus to derive programs from invariants. From Dijkstra's time we've seen partial adoptions and spinoffs from these insights. Using lambda calculus and static types gets you program behavior that looks a lot like refinement calculus and invariants (since types label domains that are equivalent to predicate sets, and lambda calculus computation is the substitution model). For that reason I would say that the spiritual successor's to Dijsktra are in the functional programming community, particularly Haskell and Scala: Erik Meijer, Richard Bird, Martin Sapolsky, etc. Carnegie Mellon's Computer Science curriculum is also fairly integrated across the board to use this style of programming and mathematics.

User23 5y ago
> The key insight of Dijkstra is that we should use a kind of substitution calculus to derive programs from invariants. It baffles me that the "formal methods" (it really should be called automated methods) crowd not only ignores this lesson, but is completely blind to it. In my direct experience, the ones I've spoken to are so obsessed with verification that the idea of constructing a program that has specified properties apparently isn't even thinkable for them. Perhaps it's a defect in my ability to explain things, but I've never once managed to explain to one of them that construction is a significantly easier task than verification. It's a real shame because they're very intelligent people that I'm certain could contribute greatly to formal program derivation. I suppose it's one of those "professional deformations" Dijkstra occasionally mentions. One of the things I'd like to do when I have copious free time is build an Emacs mode that only allows edits that preserve the given invariants, perhaps using TLA+ or something similar. Anyone that wants to learn more on the subject of deriving programs should read one or both of A Discipline of Programming[1] and Predicate Calculus and Program Semantics[2]. The former is more approachable for the programmer who isn't as inclined toward formal mathematics. The latter basically takes the same concepts and treats them with much greater mathematical rigor. [1] https://www.goodreads.com/book/show/2276288.A_Discipline_of_Programming https://www.goodreads.com/book/show/2276288.A_Discipline_of_... [2] https://www.goodreads.com/book/show/3144463-predicate-calculus-and-program-semantics https://www.goodreads.com/book/show/3144463-predicate-calcul...
- rramadass 5y ago
  >Anyone that wants to learn more on the subject of deriving programs should read Two more; * EWD316 - A Short Introduction to the Art of Programming. * A Method of Programming - Book co-authored with W.H.J.Feijen. For some reason, this is not well known though it was written as a course textbook. Draft version here: https://www.softwareresearch.net/fileadmin/src/docs/teaching/WS08/SE/A_Method_of_Programming_1.pdf https://www.softwareresearch.net/fileadmin/src/docs/teaching...
rramadass 5y ago
Great insight! His idea of the "Weakest Precondition Calculus" is Functional in contrast to "Hoare Triples" which are Relational.

User23 5y ago

Leslie Lamport immediately comes to mind. His work extending predicate transformers for concurrency[1] is a good example. Edit: Tony Hoare isn't a successor, but he's a living genius who shares many of Dijkstra's inclinations. [1] https://lamport.azurewebsites.net/pubs/lamport-win.pdf https://lamport.azurewebsites.net/pubs/lamport-win.pdf