“The act of describing a program in unambiguous detail and the act of programming are one and the same.” - Kevlin Henney
While I mostly agree with this quote, please note that it doesn't mean our formal programming languages can't be improved to feel more "natural" (actually, we've been doing this for decades).
BDD test definitions are the one that really annoy me. As far as I can tell, they're written in "natural language" (i.e. a blessed set of specific parameterizable phrases) purely so that they can be written by PMs rather than devs. If that has ever actually happened in the entire history of anything, I haven't witnessed it.
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.
Also, some things are so hard to specify formally that we still don't know have any kind of formal spec. Memory concurrency semantics is an example. It is only in the last couple of years that we got a good spec of fixed size memory accesses. Then Peter Sewell's group drops the bombshell that if you have mixed size memory accesses then you can't make programs sequentially consistent even if you add a memory barrier after every single memory access. But we still don't know how to formally specify the memory orderings associated with atomic accesses, instruction fetches, page table walks or device accesses. So, until then, we use the best natural language definition we can and hope we will be able to formalise it soon.
Also, there are parts of the natural language spec that I had not seen any value in... until I started worrying about whether the spec itself was correct or could possibly be shown to be correct. And now that I do worry about that, I am seeing new value in those parts.
[+] [-] gerbilly|8 years ago|reply
The hard part of programming is specifying the problem in an unambiguous way.
If anything natural languages can make this harder to accomplish.
[+] [-] Ace17|8 years ago|reply
While I mostly agree with this quote, please note that it doesn't mean our formal programming languages can't be improved to feel more "natural" (actually, we've been doing this for decades).
[+] [-] mrec|8 years ago|reply
[+] [-] tluyben2|8 years ago|reply
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|8 years ago|reply
[+] [-] Ace17|8 years ago|reply
Architectural intent can be expressed in a formal way, but it requires a formal language that allows you to define new abstractions.
And designing such a language is way harder than defining a small DSL with just enough features to formally express your specification.
[+] [-] adreid|8 years ago|reply
Also, some things are so hard to specify formally that we still don't know have any kind of formal spec. Memory concurrency semantics is an example. It is only in the last couple of years that we got a good spec of fixed size memory accesses. Then Peter Sewell's group drops the bombshell that if you have mixed size memory accesses then you can't make programs sequentially consistent even if you add a memory barrier after every single memory access. But we still don't know how to formally specify the memory orderings associated with atomic accesses, instruction fetches, page table walks or device accesses. So, until then, we use the best natural language definition we can and hope we will be able to formalise it soon.
Also, there are parts of the natural language spec that I had not seen any value in... until I started worrying about whether the spec itself was correct or could possibly be shown to be correct. And now that I do worry about that, I am seeing new value in those parts.