And ... so what? Nobody ever said specs are error free or complete. Heck, you didn't even get into liveness, dead lock issues.

The salient question: is risk reduced for the time alotted to write a spec in say spin or tla+?

Formal specs are risk reduction not magic.

▲

akoboldfrying 3 days ago | parent [-]

> And ... so what?

If you don't think clearly elucidating the specific issue holding back wider adoption of an otherwise amazing technology is relevant to this discussion, I don't know what to tell you.

	▲	scrubs 2 days ago \| parent \| next [-]
		I'm currently writing a formal model for a packet protocol in tla. (I started with spin). And im writing a paper with my findings including some thoughts on why FM are not more widely adopted. here academics and FM system devs have work to do. But let me tend to the other side: industrial developers: FM requires attention to detail in order to leverage the power of LTL etc. You mention a few things about sorting which are important details. Too many devs I think are a bit lazy here. HW does better as a discipline ... software devs no so much. FM more than vanilla coding requires attention to many small issues eg fairness. I think that too easily scares off some devs. Also writing a tla model requires a different mind set from imperative coding. Devs see that and are too allergic to learning.
	▲	cwillu 3 days ago \| parent \| prev [-]
		Indeed, it's a microcosm of the same problem.