5 ms·

Where are formal methods used in industry? To quote http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html http://research.microsoft.com/en-us/u

Where are formal methods used in industry? To quote http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html http://research.microsoft.com/en-us/um/people/lamport/tla/am... - "We have found relatively little published literature on using high-level formal specification to verify the design of complex distributed systems in industry."

mlitchard 12y ago
Here https://www.facebook.com/ https://www.facebook.com/ Here https://galois.com/ https://galois.com/ And Here https://www.fpcomplete.com/ https://www.fpcomplete.com/ To name a few.
- danblick 12y ago
  Could you elaborate on the uses at Facebook?
  - gohrt 12y ago
    https://code.facebook.com/posts/302060973291128/open-sourcing-haxl-a-library-for-haskell/ https://code.facebook.com/posts/302060973291128/open-sourcin...
    - mlitchard 12y ago
      Also, This guy https://www.youtube.com/watch?v=ZR3Jirqk6W8 https://www.youtube.com/watch?v=ZR3Jirqk6W8 had his Haskell startup bought by Facebook. I expect it was because they wanted the technology he invented, and him as well.
    - gelisam 12y ago
      While Haxl is great and is a good example of Haskell usage in the industry, it's not a good example of the usage of formal methods, since functional programming is only the first of the two steps mentioned in the article. The title of this post made me hope they were looking to hire a "proof engineer", but alas, they're only explaining how to become one. It's already hard enough trying to find a Haskell job, finding one in Isabelle or Agda must be near impossible!
munin 12y ago
it is used some in aerospace and defense: https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/FMICS07-Rockwell-Collins.pdf https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/FMIC... I have heard stories from people in Europe that formal methods are used there in checking implementations for life and safety critical pieces of civil engineering, like high speed trains and nuclear power stations.
Jtsummers 12y ago
Some examples with Spark and Ada [1]. Wish they had more listed. I know of read about some other development projects using Spark but my google-fu is weak today. [1] http://www.adacore.com/sparkpro/projects http://www.adacore.com/sparkpro/projects

mlitchard 12y ago

Here https://www.facebook.com/ https://www.facebook.com/ Here https://galois.com/ https://galois.com/ And Here https://www.fpcomplete.com/ https://www.fpcomplete.com/ To name a few.

danblick 12y ago
Could you elaborate on the uses at Facebook?
- gohrt 12y ago
  https://code.facebook.com/posts/302060973291128/open-sourcing-haxl-a-library-for-haskell/ https://code.facebook.com/posts/302060973291128/open-sourcin...
  - mlitchard 12y ago
    Also, This guy https://www.youtube.com/watch?v=ZR3Jirqk6W8 https://www.youtube.com/watch?v=ZR3Jirqk6W8 had his Haskell startup bought by Facebook. I expect it was because they wanted the technology he invented, and him as well.
  - gelisam 12y ago
    While Haxl is great and is a good example of Haskell usage in the industry, it's not a good example of the usage of formal methods, since functional programming is only the first of the two steps mentioned in the article. The title of this post made me hope they were looking to hire a "proof engineer", but alas, they're only explaining how to become one. It's already hard enough trying to find a Haskell job, finding one in Isabelle or Agda must be near impossible!

munin 12y ago

it is used some in aerospace and defense: https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/FMICS07-Rockwell-Collins.pdf https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/FMIC... I have heard stories from people in Europe that formal methods are used there in checking implementations for life and safety critical pieces of civil engineering, like high speed trains and nuclear power stations.

Jtsummers 12y ago

Some examples with Spark and Ada [1]. Wish they had more listed. I know of read about some other development projects using Spark but my google-fu is weak today. [1] http://www.adacore.com/sparkpro/projects http://www.adacore.com/sparkpro/projects