4 ms·

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 c

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).
  - nickpsecurity 10y ago
    Re meyer The neat thing is his method was adopted commercially with years of success despite never showing up on Hacker News, etc. It combined efficiency, OOP, basic safety, and concurrency safety (SCOOP). Most talk about adoption of formal specs in theory but he got it done in practice with DbC in industry. Now, tools like SPARK, Ada 2012, and Perfect Developer are using it. You can do it in C, C# and Java, too. Btw, in case you missed it, his Theory of Programs defines most aspects of programming in an elegant, precise way using set theory: https://arxiv.org/pdf/1507.00723v3 https://arxiv.org/pdf/1507.00723v3 Re dependent Learn from the master: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ Far as whether they're good, Im not sure as formal methodists have endless arguments on it. The critics basically say you have to put in enough spec and proving work that you might as well do the real thing in a prover then extract it. Chlipala actually does something like that called Programs as Proofs I think. Memory gettimg fuzzy. Just remember dependent types vs proving is in dispute at the moment.

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).
- nickpsecurity 10y ago
  Re meyer The neat thing is his method was adopted commercially with years of success despite never showing up on Hacker News, etc. It combined efficiency, OOP, basic safety, and concurrency safety (SCOOP). Most talk about adoption of formal specs in theory but he got it done in practice with DbC in industry. Now, tools like SPARK, Ada 2012, and Perfect Developer are using it. You can do it in C, C# and Java, too. Btw, in case you missed it, his Theory of Programs defines most aspects of programming in an elegant, precise way using set theory: https://arxiv.org/pdf/1507.00723v3 https://arxiv.org/pdf/1507.00723v3 Re dependent Learn from the master: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ Far as whether they're good, Im not sure as formal methodists have endless arguments on it. The critics basically say you have to put in enough spec and proving work that you might as well do the real thing in a prover then extract it. Chlipala actually does something like that called Programs as Proofs I think. Memory gettimg fuzzy. Just remember dependent types vs proving is in dispute at the moment.