4 ms·

Well it's not popular (even though it ought to be), but Edsger Dijkstra's A Discipline of Programming is an approachable and informal (by the author's standards

by User23 3y ago

Well it's not popular (even though it ought to be), but Edsger Dijkstra's A Discipline of Programming is an approachable and informal (by the author's standards) look at solving non-trivial problems in a provably correct way. In fact the entire EWD archive[1] can be arranged into a course pretty readily, although you'll definitely want to skim or skip large chunks of it. Also some of the papers are just acerbic observations on life, which some people like and some don't. And there's it's big brother Predicate Calculus and Program Semantics by Dijkstra and Scholten that more rigorously formalizes the same approach. Dafny[2] is one approach out of Microsoft Research that attempts to provide automated tooling around some of those concepts. All of the above are excellent places to start if you're interested in learning how to write better code with the imperative languages that you're actually going to use professionally. [1] https://www.cs.utexas.edu/users/EWD/ https://www.cs.utexas.edu/users/EWD/ [2] https://dafny.org/ https://dafny.org/

sn9 3y ago
You can use Coq to teach yourself many of the same ideas from ADP using Penn's Software Foundations (probably the first two books are sufficient). A somewhat more modern approach of related concepts to ewd's work is the work of Richard Bird which teaches you about using equational reasoning to take a correct naive algorithm and systematically optimize it into a correct and fast algorithm. [0] [1] Regarding Dafny, there's actually a new book out that should be approachable to anyone with programming experience. [2] [0] https://www.cs.ox.ac.uk/publications/books/functional/ https://www.cs.ox.ac.uk/publications/books/functional/ [1] https://www.cs.ox.ac.uk/publications/books/adwh/ https://www.cs.ox.ac.uk/publications/books/adwh/ [2] https://mitpress.mit.edu/9780262546232/program-proofs/ https://mitpress.mit.edu/9780262546232/program-proofs/
- User23 3y ago
  One of the real eye openers for me along that journey was realizing that Eclipse refactors were (mostly, except for some rough edges) automated semantic invariant preserving code transformations, which is to say a kind of simplified equational reasoning resting solely on the equivalence. Equational reasoning is borderline magical, and I look forward to the day when it's as pervasively taught as basic logic. I have this fantasy in my mind of a language/editor combination that begins with the empty program and only allows legal equational development. Without explicit predication that would just maintain the invariants of the language itself, so no undefined behaviors, but with user supplied predicates would allow a kind of exploratory programming with safety nets. One way to look at it would be explicit symmetry breaking, although I'm not sure that's a good way to describe it to typical working programmers. The idea though is that for a program with the empty specification all code transformations are symmetrical with respect to the spec. And then as the specification is added to certain transformations become symmetry breaking and thus illegal, with said illegality being statically checked. Clearly I'm waving my hands quite a lot here, and I have no clue if it's actually practicable.

by User23 3y ago

sn9 3y ago

You can use Coq to teach yourself many of the same ideas from ADP using Penn's Software Foundations (probably the first two books are sufficient). A somewhat more modern approach of related concepts to ewd's work is the work of Richard Bird which teaches you about using equational reasoning to take a correct naive algorithm and systematically optimize it into a correct and fast algorithm. [0] [1] Regarding Dafny, there's actually a new book out that should be approachable to anyone with programming experience. [2] [0] https://www.cs.ox.ac.uk/publications/books/functional/ https://www.cs.ox.ac.uk/publications/books/functional/ [1] https://www.cs.ox.ac.uk/publications/books/adwh/ https://www.cs.ox.ac.uk/publications/books/adwh/ [2] https://mitpress.mit.edu/9780262546232/program-proofs/ https://mitpress.mit.edu/9780262546232/program-proofs/

User23 3y ago
One of the real eye openers for me along that journey was realizing that Eclipse refactors were (mostly, except for some rough edges) automated semantic invariant preserving code transformations, which is to say a kind of simplified equational reasoning resting solely on the equivalence. Equational reasoning is borderline magical, and I look forward to the day when it's as pervasively taught as basic logic. I have this fantasy in my mind of a language/editor combination that begins with the empty program and only allows legal equational development. Without explicit predication that would just maintain the invariants of the language itself, so no undefined behaviors, but with user supplied predicates would allow a kind of exploratory programming with safety nets. One way to look at it would be explicit symmetry breaking, although I'm not sure that's a good way to describe it to typical working programmers. The idea though is that for a program with the empty specification all code transformations are symmetrical with respect to the spec. And then as the specification is added to certain transformations become symmetry breaking and thus illegal, with said illegality being statically checked. Clearly I'm waving my hands quite a lot here, and I have no clue if it's actually practicable.