Re:Are natural language specifications useful?
by balfirevic on Monday August 21, 2017 @01:53PM
(#15066259)
Can you share more about what kind of programs you're specifying with TLA+? Business applications, particular algorithms, or something else entirely?
Re:Are natural language specifications useful?
by tluyben2 on Monday August 21, 2017 @10:57PM
(#15069390)
Our 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.
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.