3 ms·
We started with everything in natural on our products, but rapidly I found myself wanting something more formal. I have been working on formal specs for our pr
by tluyben2 9y ago
We started with everything in natural on our products, but rapidly I found myself wanting something more formal.
I have been working on formal specs for our products in Coq in the past but it took me too much time and outside solely software dev it got me stuck.
So lately I have been using TLA+ (I used it many years ago but did not find it formal enough in my then naive age and experience) and I must say it is great.
The learning curve is quite steep but not as steep as Idris or Coq (also less formal) and far more practical.
Think the author could have used TLA+ although I did not get a full appreciation about his executable specs from that article.
- balfirevic 9y agoCan you share more about what kind of programs you're specifying with TLA+? Business applications, particular algorithms, or something else entirely?
- tluyben2 9y agoOur firmware, encryption algorithms, app/web and deployments. I currently finished the firmware and deployments and working on the rest now. The firmware helped a lot as we cannot change that in the field so we need to agree on a non ambiguous way of communicating the specs for it.