3 ms·

I have a MSc with a specialization in formal methods from a place with famous faculty in the field, so I might be biased. But I have to disagree with almost any

by nextos 8y ago

I have a MSc with a specialization in formal methods from a place with famous faculty in the field, so I might be biased. But I have to disagree with almost anyone here. Formal methods still lack a bit of maturity and streamlining to get adopted. It's a bit like functional programming in the late 90s and early 2000s. Nothing was terribly different from now, yet it was not widely used. Whereas now, we are starting to see adoption by mainstream players. E.g. lots of features in Swift. With regards to formal methods, the situation is entirely analogous. The theory is there. Already developed. And it sits at the absolute core of CS. It's all about formally describing semantics. There are several approaches: type systems, model checking, program analysis and abstract interpretation. And these offer a tremendous amount of flexibility. You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms.

jlelonm 8y ago
> You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms. This statement particularly interested me. If I wanted to learn more about this, what resources do you recommend? If you ask how deep I want to go, let's say we have a scale of abstraction that's from 1 to 10, where 1 is a two paragraph executive summary and 10 is an entire Ph.D's worth of training. I'd probably be looking at a 2.5 to a 5.
- nextos 8y ago
  Some references below. You'd probably want to start with the first 3. The other 3 are classics, but much more dense (e.g. the Nielsons book requires some decent abstract algebra background): * Software Foundations (Pierce): https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ * Concrete Semantics (Nipkow): http://www21.in.tum.de/~nipkow/Concrete-Semantics/ http://www21.in.tum.de/~nipkow/Concrete-Semantics/ * FRAP (Chlipala): http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/ * Model checking (Katoen): https://mitpress.mit.edu/books/principles-model-checking https://mitpress.mit.edu/books/principles-model-checking * Program analysis & abstract interpretation (the Nielsons): https://www.springer.com/gb/book/9783540654100 https://www.springer.com/gb/book/9783540654100 * Type systems (Pierce): https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
pron 8y ago
Judging by the reading list you've provided below, you may not be familiar with more "productized" formal methods, designed for use by working engineers, like TLA+ and Alloy. I don't know if I'd call them entirely "mature" yet, but they are certainly industrial-strength, learned by ordinary programmers in 2-3 weeks of part-time reading of tutorials or in a few days with guidance, after which they go on to specify and verify large, complex real-world systems. Lamport spent years simplifying TLA+ and designing it for user-friendliness (at the cost of making it inappropriate for logicians to do research on novel logics). While extremely powerful (people have implemented TLA in Isabelle and Coq to reason about concurrent and interactive systems), it is based mostly on ordinary, high-school or first-year-college math, and entirely eschews the complications of programming language semantics. See the following industry reports: * Amazon: http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf http://lamport.azurewebsites.net/tla/formal-methods-amazon.p... -- this has been so successful that managers encourage developers to use TLA+ to reduce development costs. * Microsoft: https://youtu.be/ifFfxRCX_jw https://youtu.be/ifFfxRCX_jw * https://youtu.be/tfnldxWlOhM https://youtu.be/tfnldxWlOhM

by nextos 8y ago

jlelonm 8y ago

> You can go all the way from adding some lightweight formal specifications a posteriori with e.g. a fancy type system, to developing all your code formally by starting with some axioms. This statement particularly interested me. If I wanted to learn more about this, what resources do you recommend? If you ask how deep I want to go, let's say we have a scale of abstraction that's from 1 to 10, where 1 is a two paragraph executive summary and 10 is an entire Ph.D's worth of training. I'd probably be looking at a 2.5 to a 5.

nextos 8y ago
Some references below. You'd probably want to start with the first 3. The other 3 are classics, but much more dense (e.g. the Nielsons book requires some decent abstract algebra background): * Software Foundations (Pierce): https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ * Concrete Semantics (Nipkow): http://www21.in.tum.de/~nipkow/Concrete-Semantics/ http://www21.in.tum.de/~nipkow/Concrete-Semantics/ * FRAP (Chlipala): http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/ * Model checking (Katoen): https://mitpress.mit.edu/books/principles-model-checking https://mitpress.mit.edu/books/principles-model-checking * Program analysis & abstract interpretation (the Nielsons): https://www.springer.com/gb/book/9783540654100 https://www.springer.com/gb/book/9783540654100 * Type systems (Pierce): https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/

pron 8y ago

Judging by the reading list you've provided below, you may not be familiar with more "productized" formal methods, designed for use by working engineers, like TLA+ and Alloy. I don't know if I'd call them entirely "mature" yet, but they are certainly industrial-strength, learned by ordinary programmers in 2-3 weeks of part-time reading of tutorials or in a few days with guidance, after which they go on to specify and verify large, complex real-world systems. Lamport spent years simplifying TLA+ and designing it for user-friendliness (at the cost of making it inappropriate for logicians to do research on novel logics). While extremely powerful (people have implemented TLA in Isabelle and Coq to reason about concurrent and interactive systems), it is based mostly on ordinary, high-school or first-year-college math, and entirely eschews the complications of programming language semantics. See the following industry reports: * Amazon: http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf http://lamport.azurewebsites.net/tla/formal-methods-amazon.p... -- this has been so successful that managers encourage developers to use TLA+ to reduce development costs. * Microsoft: https://youtu.be/ifFfxRCX_jw https://youtu.be/ifFfxRCX_jw * https://youtu.be/tfnldxWlOhM https://youtu.be/tfnldxWlOhM