Dependent-types are a more lightweight formal method. They're pretty useful as Chlipala et al showed in many developments. IDRIS and ATS languages use them for systems. Software Foundations is about the full thing.
Tried to find you an easy intro. Harder than I thought. However, this PowerPoint is an excellent intro to formal specifications in terms of what they are, why you want them, and many examples.
Once you see that, it becomes obvious that proving implementation matches such specs is beneficial. Took an hour to find an intro to that which was worthwhile and easy to digest. Here's one:
http://adam.chlipala.net/cpdt/cpdt.pdf
https://www.cis.upenn.edu/~bcpierce/sf/current/index.html
Dependent-types are a more lightweight formal method. They're pretty useful as Chlipala et al showed in many developments. IDRIS and ATS languages use them for systems. Software Foundations is about the full thing.
Tried to find you an easy intro. Harder than I thought. However, this PowerPoint is an excellent intro to formal specifications in terms of what they are, why you want them, and many examples.
http://www.cs.nott.ac.uk/~pszrq/files/1FSPintroduction.ppt
Once you see that, it becomes obvious that proving implementation matches such specs is beneficial. Took an hour to find an intro to that which was worthwhile and easy to digest. Here's one:
http://www2.imm.dtu.dk/~aeha/Railway/index/TSnotat.pdf
Anyone following along that wants a list of tools, esp open-source, should check out Wheeler's reference on high-assurance FLOSS:
http://www.dwheeler.com/essays/high-assurance-floss.html