SPIN's language Promela is very odd, like stripped down basic from the 1980s but even more reduced after that.
Edit: a bit more from the spin site FYI "[spin] checks the logical consistency of a specification and reports on deadlocks, race conditions, different types of incompleteness, and unwarranted assumptions about the relative speeds of processes"
I wish so much I had reason to use it. I so much wish my programming career wasn't the daily, usually boring, straightforward business support. I'd love to work with TLA, formal methods, this and more but there seems no way to do get a job doing this. Any thoughts welcome. Been trying to learn hoare logic but it all seems so abstract, and it's easy to misunderstand things with no-one to ask. Anyway, sorry for the whinge.
I think the typical business software could be a great place to start because you have sections of the code that would be very simple to model in a formal methods environment and that really hairy section that could actually use it (but it would be hard).
I hate to say I've never had the patience for it. For me it has always turned out to be painful without much reward.
I think my experience isn't uncommon given the popularity of formal methods. If it was easy and full of low hanging fruit (like automated testing) it would probably be reasonably popular (like automated testing).
I dunno where in business software it might work, but my experience is that quality is often almost irrelevant. A few weeks ago I got myself unpopular for finding and reporting a serious bug. That could have been picked up through a little knowledge or some straightforward testing, but it wasn't because that didn't happen (there's a little more to it than that, but you see my point). If producing crap is acceptable, there's no room for formal methods. I've had a lot of experience of this.
If you can't get the boss's buy-in for even obvious correctness and/or timesaving approaches (where time spent = salaries paid), I'm stuffed.
Or maybe the problem's partly me. I can't rule that out. I'm not the most politic person.
> If [formal methods] was easy and full of low hanging fruit...
It isn't and I don't expect it to be. The fruit is right at the top, but it may be the best quality. I'm ok putting in the work to reach that.
Spin homepage http://spinroot.com/spin/whatispin.html
SPIN's language Promela is very odd, like stripped down basic from the 1980s but even more reduced after that.
Edit: a bit more from the spin site FYI "[spin] checks the logical consistency of a specification and reports on deadlocks, race conditions, different types of incompleteness, and unwarranted assumptions about the relative speeds of processes"
I wish so much I had reason to use it. I so much wish my programming career wasn't the daily, usually boring, straightforward business support. I'd love to work with TLA, formal methods, this and more but there seems no way to do get a job doing this. Any thoughts welcome. Been trying to learn hoare logic but it all seems so abstract, and it's easy to misunderstand things with no-one to ask. Anyway, sorry for the whinge.