4 ms·

Formal methods. Extremely cool and undervalued, except on a few key and well paying industries. I believe it will make a big comeback when it's more ready for p

by nextos 9y ago

Formal methods. Extremely cool and undervalued, except on a few key and well paying industries. I believe it will make a big comeback when it's more ready for prime time. You can start small and grow your skills in many directions: linear types, probabilistic model checking... It involves a very neat but approachable branch of mathematics: abstract algebra.

DennisP 9y ago
I didn't realize abstract algebra was related to formal methods. Would learning the math first make it easier? Formal methods are on the verge of being a big thing in smart contract programming, where the code is short and failures are expensive.
- nextos 9y ago
  Knowing a bit of abstract algebra, semantics and type theory doesn't hurt. But I'd suggest to start by reading http://www.concrete-semantics.org/ http://www.concrete-semantics.org/, which is a great overview. Once done, you can go for an approach well-grounded on the theories I mentioned above. I agree formal methods are great for smart contracts. Back in '08 when I was doing graduate work on the topic, some researchers were already talking about it, but the enabling technology (blockchain) was missing. They are also great for real-time critical systems, especially if you go with a formal methodology, where you start with some axioms (e.g. two trains can't be in the same track partition) and progressively derive your system from these by applying formally verified transformations till you end up with the code to deploy.
  - DennisP 9y ago
    Downloaded it and ordered the paper copy, thanks :)
bostonvaulter2 9y ago
What would you advise looking into in regards to formal methods? Any particular software, books, or talks?
- nextos 9y ago
  Concrete Semantics is an excellent free book http://www.concrete-semantics.org/ http://www.concrete-semantics.org/ written by some well-known names in the field. It's a good place to begin. The book itself contains references to much more advanced works such as Nielson & Nielson or TAPL. It doesn't cover one part of formal methods, (probabilistic) model checking.
  - sevensor 9y ago
    Thanks for this -- I've been looking for recommendations on resources for HOL and this looks like a good one.

by nextos 9y ago

DennisP 9y ago

I didn't realize abstract algebra was related to formal methods. Would learning the math first make it easier? Formal methods are on the verge of being a big thing in smart contract programming, where the code is short and failures are expensive.

nextos 9y ago
Knowing a bit of abstract algebra, semantics and type theory doesn't hurt. But I'd suggest to start by reading http://www.concrete-semantics.org/ http://www.concrete-semantics.org/, which is a great overview. Once done, you can go for an approach well-grounded on the theories I mentioned above. I agree formal methods are great for smart contracts. Back in '08 when I was doing graduate work on the topic, some researchers were already talking about it, but the enabling technology (blockchain) was missing. They are also great for real-time critical systems, especially if you go with a formal methodology, where you start with some axioms (e.g. two trains can't be in the same track partition) and progressively derive your system from these by applying formally verified transformations till you end up with the code to deploy.
- DennisP 9y ago
  Downloaded it and ordered the paper copy, thanks :)

bostonvaulter2 9y ago

What would you advise looking into in regards to formal methods? Any particular software, books, or talks?

nextos 9y ago
Concrete Semantics is an excellent free book http://www.concrete-semantics.org/ http://www.concrete-semantics.org/ written by some well-known names in the field. It's a good place to begin. The book itself contains references to much more advanced works such as Nielson & Nielson or TAPL. It doesn't cover one part of formal methods, (probabilistic) model checking.
- sevensor 9y ago
  Thanks for this -- I've been looking for recommendations on resources for HOL and this looks like a good one.