4 ms·

> In fact, code is a nasty byproduct of being a software engineer. This is the core of the matter. This is something Dijkstra, Edward Cohen, Jayadev Misra, an

> In fact, code is a nasty byproduct of being a software engineer. This is the core of the matter. This is something Dijkstra, Edward Cohen, Jayadev Misra, and others in and around the formal methods camp have been saying for decades. It is more worthwhile to solve the problem than to guess your program into existence and patch the errors later. To dismiss them is to say you do not appreciate the true difficulty of programming and designing systems. In practice I don't write formal proofs for every line of code -- how exhausting! But I do often write high-level specifications in tandem with the software I'm using to implement it and often one informs the other to the true nature of the problem I'm trying to solve. And I find that as I improve in different logics and predicate calculus I can find and spot the design errors in the structures formed by code that you don't see if all you're doing is trying to "solve the puzzle." The whole approach to guessing your program and patching the bugs later is far too addictive. It saddens me when otherwise good programmers fall into this trap. It creates work for oneself but it keeps you from solving the real problem at hand! Nice article. Not sure about the allure of "Taco Bell," but the spirit is in the right place.

rpazyaquian 10y ago
Where can I read more about this? "Formal methods"? Being able to write proofs and tests/frameworking around things that I need to write would help me be more confident in what I do and also help me keep myself on track/not end up going down rabbit holes.
- agentultra 10y ago
  Programming in the 1990s by Edward Cohen is an interesting book for introducing software developers to a method of proof writing by way of predicate calculus. It's a book one can read from cover to cover. The TLA+ book by Leslie Lamport is also an interesting read even if it is specific to a particular logic for creating specifications. Any of his talks on TLA+ are also good for a high-level overview of the why and a bit of the how as well.
- shubb 10y ago
  Most people are writing business logic not algorithms (a website not a video encoder). If that's you, you should also check out BDD esp frameworks like cucumber, as that may be useful.
- nickpsecurity 10y ago
  There's several, different kinds you might use. One group are designed for formal specification rather than verification where you're mainly making it easier to understand for people with some tool checking. Another type is designed to help a formal logic prove specific things about your software. Then, there's lighter versions like model checkers that explore abstract models of the system to prove properties about it but operate on constrained problems. Here's an introduction to Z specification language that illustrates how it uses simple formalism to precisely specify requirements and design going from abstract to concrete: https://people.csail.mit.edu/dnj/teaching/6898/papers/spivey-intro-to-z.pdf https://people.csail.mit.edu/dnj/teaching/6898/papers/spivey... Alloy is a model-checker in a similar vein as Z that's designed for easier use and automation: https://www.doc.ic.ac.uk/project/examples/2007/271j/suprema_on_alloy/Final%20Report/LaTeX/report.pdf https://www.doc.ic.ac.uk/project/examples/2007/271j/suprema_... Although TLA+ is popular now, SPIN was the goto model-checker for analyzing software for concurrency errors: http://www2.imm.dtu.dk/courses/02152/CP/spin.pdf http://www2.imm.dtu.dk/courses/02152/CP/spin.pdf Software Foundations teaches you formal verification of the kind that is used in cutting-edge academic projects like CompCert compiler or seL4 kernel: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html Language designers can also include lightweight, formal methods into their type systems like Design by Contract which helps knock out interface/integration errors: https://www.eiffel.com/values/design-by-contract/introduction/ https://www.eiffel.com/values/design-by-contract/introductio... Finally, since logic programming is so fast these days, one can even translate logical specs into logical programs to straight-up execute the specification: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.34.6816&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.34.... Note: The Z, Allow, SPIN, and Coq tools referenced above all have websites with FOSS software, tutorials, etc. Just Google them.
  - agentultra 10y ago
    Eiffel, I hear, was (is?) quite cool. I've read some of Bertrand Meyer's work and have learned a lot from it. One area that is becoming really interesting to me is in dependently typed languages and their ability to encode at least some of the properties of the formal specification in the type system. I haven't had much time to take a deep dive into Agda but what I have challenged myself with gives me hope that this may be the way we write programs in the future (even if it's not Agda per se).

rpazyaquian 10y ago

Where can I read more about this? "Formal methods"? Being able to write proofs and tests/frameworking around things that I need to write would help me be more confident in what I do and also help me keep myself on track/not end up going down rabbit holes.

agentultra 10y ago
Programming in the 1990s by Edward Cohen is an interesting book for introducing software developers to a method of proof writing by way of predicate calculus. It's a book one can read from cover to cover. The TLA+ book by Leslie Lamport is also an interesting read even if it is specific to a particular logic for creating specifications. Any of his talks on TLA+ are also good for a high-level overview of the why and a bit of the how as well.
shubb 10y ago
Most people are writing business logic not algorithms (a website not a video encoder). If that's you, you should also check out BDD esp frameworks like cucumber, as that may be useful.
nickpsecurity 10y ago
There's several, different kinds you might use. One group are designed for formal specification rather than verification where you're mainly making it easier to understand for people with some tool checking. Another type is designed to help a formal logic prove specific things about your software. Then, there's lighter versions like model checkers that explore abstract models of the system to prove properties about it but operate on constrained problems. Here's an introduction to Z specification language that illustrates how it uses simple formalism to precisely specify requirements and design going from abstract to concrete: https://people.csail.mit.edu/dnj/teaching/6898/papers/spivey-intro-to-z.pdf https://people.csail.mit.edu/dnj/teaching/6898/papers/spivey... Alloy is a model-checker in a similar vein as Z that's designed for easier use and automation: https://www.doc.ic.ac.uk/project/examples/2007/271j/suprema_on_alloy/Final%20Report/LaTeX/report.pdf https://www.doc.ic.ac.uk/project/examples/2007/271j/suprema_... Although TLA+ is popular now, SPIN was the goto model-checker for analyzing software for concurrency errors: http://www2.imm.dtu.dk/courses/02152/CP/spin.pdf http://www2.imm.dtu.dk/courses/02152/CP/spin.pdf Software Foundations teaches you formal verification of the kind that is used in cutting-edge academic projects like CompCert compiler or seL4 kernel: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html Language designers can also include lightweight, formal methods into their type systems like Design by Contract which helps knock out interface/integration errors: https://www.eiffel.com/values/design-by-contract/introduction/ https://www.eiffel.com/values/design-by-contract/introductio... Finally, since logic programming is so fast these days, one can even translate logical specs into logical programs to straight-up execute the specification: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.34.6816&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.34.... Note: The Z, Allow, SPIN, and Coq tools referenced above all have websites with FOSS software, tutorials, etc. Just Google them.
- agentultra 10y ago
  Eiffel, I hear, was (is?) quite cool. I've read some of Bertrand Meyer's work and have learned a lot from it. One area that is becoming really interesting to me is in dependently typed languages and their ability to encode at least some of the properties of the formal specification in the type system. I haven't had much time to take a deep dive into Agda but what I have challenged myself with gives me hope that this may be the way we write programs in the future (even if it's not Agda per se).