Why Don't People Use Formal Methods?

General Prog (Archived)
,
3

It is slightly broken but can be deciphered.

https://news.ycombinator.com/item?id=18965274

2 Likes
4

Thanks. HN is blocked from where I work, you can find the discussion with google “Hacker news” “Why Don’t People Use Formal Methods?” or https://webcache.googleusercontent.com/search?q=cache:5b7NjC3_7XYJ:https://news.ycombinator.com/item%3Fid%3D18965274+&cd=1&hl=en&ct=clnk&gl=nl
I’ll look for the direct link when I’m home and correct it.

1 Like
5

This has been a fascinating subject to me of late. There are a few talks on youtube from the same author. I found this one really interesting:

4 Likes
6

Short answer is: people find it too hard, or they don’t have the time/resources to learn better.

I’m falling in the second camp but I really want to learn all the math that is needed for formal verification. And then apply the knowledge in programming.

Anybody has a learning onboarding suggestion? I can learn math just fine – never had trouble with it. But I lack a good educational plan to get to the formal methods.

2 Likes
7

That was a good read. Thanks for sharing. I really need to block off some more time to learn more about TLA+ (and other formal methods)

5 Likes
8

Here’s a tweet about how the blog writer came to formal methods:


In his blog he names a tutorial he wrote, he organizes workshops too: https://www.hillelwayne.com/post/practical-tla/ https://www.apress.com/us/book/9781484238288 . There is also
https://lamport.azurewebsites.net/video/videos.html

1 Like
9
  • The art is not much asked for in vacancies. To become popular you should do a scrum course, learn the atlassian toolsuite (jira and all) and java. :wink:
    For the suggestions see Why Don't People Use Formal Methods? (+ google is your friend).
10

But I’m not interested in job vacancies, not sure where you got that from. :017:

I’m interested in intro courses. Gentle introductions if you will.

11

I supplied an extra reason for “Why Don’t People Use Formal Methods?”. “You” is meant in the general sense, like “one”. Hahaha.

12

My bad. :003:

I’m still interested in learning materials though!

13

Besides the book that StefanHoutzager already linked, how about some free materials:

https://learntla.com - website that teaches TLA+ basics

http://lamport.azurewebsites.net/tla/learning.html - website of TLA+ creator with free book and even a free video course

3 Likes
14

Is the TLA+ the only way to practice formal methods?

15

Depends on what you want to do, there is also Coq, Idris, Agda, etc.

My biggest gripe with formal languages is fact that the learning materials are troublesome. I mean, ok. there is LearnTLA book, but it jumps directly to writing proofs totally omitting how to install and configure environment, it just assumes that you already have one. The same goes for other languages.

Additionally these materials often assume that I have some theoretical knowledge, while it isn’t bad thing, it would be worth to describe what I need to know a priori and provide me links to some materials where I can learn about it before continue.

And about LearnTLA my gripe is that it mixes PlusCal and TLA+ without clearly stating why there are two syntaxes and what is their relation, it just states that “PlusCal is preferred way to write code”, but why so? Not a clue, it just is.

Some time ago I tried to learn Agda and Coq and there also were problems like that where it goes like:

  • you write that - ok I follow
  • this mean that XY - ok, not bad
  • then you write this do_zygohistomorphic_prephomorphism; and you get result - WTF just happened

I have feeling that these tools assume, that you know what you want to do and they just describe how to write it in the form of code, not that you want to learn how to write and understand that proofs.

Also some book/examples that shows how to write proofs from code or how to write code from proofs (even on very abstract level) would be nice, this could help in broader use.

6 Likes
16

Google is my friend + I know that I know nothing (google: this stems from Socrates) :wink: => https://en.wikipedia.org/wiki/Formal_specification names a couple more

17

This – and frankly your entire comment – hits the nail on the head. I wanted to start getting good in this area several times in the last 2.5 years but every time I am struck by that exact mindset: “you already studied the math, you know exactly which theorems and formulae to use, now we propose a way to apply them to software in language X using very specialized tool Y”. And I just end up throwing my hands in the air and quitting, every time so far.

Many people can learn the math and the needed mechanisms in it to start working on formal proofs and verification – but the literature and software do absolutely nothing to onboard you.

So if that HN thread wasn’t as crowded as it was I’d try to just answer this:

Because nobody makes an effort to walk you from start to end and treat you like an actual student.

…and would probably end up being downvoted to hell. :003:

3 Likes
18

There are usergroups. This one for tla+ f.e. looks active: https://groups.google.com/forum/#!forum/tlaplus
Lamport himself writes in this group too. He comments on Hillels book here https://lamport.azurewebsites.net/tla/practical-tla.html?back-link=learning.html#hillel?unhideBut@EQhide-hillel@AMPunhideDiv@EQhillel
It might be that f.e. Hillel answers question via mail or twitter. An installation guideline you can find immediately with google: https://lamport.azurewebsites.net/tla/toolbox.html
Just interested btw, I have not tried tla+.

1 Like
19

Ok, you’ve reached the dead end already. Allas. I think there could have been some more possibilities to get into this though. :wink:

20

I would suggest starting with Z. Given its based on set theory its super easy to pick up. You don’t need all the other fancy tools other than a means of writing the notation. I had used a Word template. Although the tools are nice just taking the time to think things through especially for requirements gathering is an absolute boon.

I had borrowed a book from the library to learn it “on the job”. Given the resources online for Z the book might be optional :slight_smile:

21

Although not a formal formal method type driven design with F# or Haskell is something to look into as well. Here your axioms and code blend together and you are relying on the language compiler to model check for you.

1 Like
22

Can you give links to your preferred reading material for that Z thing, please?