Some of this we can automate, but the more expressive you want your spec to be, the less we can automate. With specs you can handwave away things like "the process of retrieving and parsing the CSV", and now you have to prove all that implementation matches the handwave.
-
Show this thread
-
Again, it's not impossible. But it's often _infeasible_: it just costs too much time and money that's better spent doing other things. Which is why in the industry, we usually just assume there's no way to connect the spec and the code. It's just an economic reality.
3 replies 0 retweets 11 likesShow this thread -
Some people find this demoralizing. I find it reassuring. It means we're not selling snake oil. We're pitching an approach that has known, understood limitations. Formal Methods isn't the magic solution to all your problems, and we're okay with this! It makes it _real_.
2 replies 0 retweets 15 likesShow this thread -
But that probably doesn't reassure you. If you can't keep the code and spec in sync, why bother? Two answers to this: 1. Specs are more expressive in code, so they're a lot smaller. A thousand line change to the code might mean only a 1-line change to the spec.
1 reply 1 retweet 15 likesShow this thread -
2. You write a bunch of code and run into a very nasty bug in prod. Would you rather know the design is correct and it must be an error in implementing the design, or have no idea whether the problem is with the code or the fundamental design?
1 reply 4 retweets 26 likesShow this thread -
Ultimately, we write specifications because it works. It saves time and money. We'd save more time and money if we had easy synthesis and refinement, but we don't, and we're realistic about our expectations. And even then, it saves time and money.https://www.hillelwayne.com/post/business-case-formal-methods/ …
1 reply 2 retweets 17 likesShow this thread -
If you want to learn more, I wrote a longer essay on the history, limitations, and developments in formal methods:https://www.hillelwayne.com/post/why-dont-people-use-formal-methods/ …
1 reply 1 retweet 14 likesShow this thread -
I also teach people these tools as my business. This was a sales pitch, srry https://www.hillelwayne.com/consulting/ In the near future I have two slots remaining for a 1-day alloy workshop:https://www.eventbrite.com.au/e/software-modeling-with-alloy-workshop-registration-104254118876?aff=erelpanelorg …
2 replies 2 retweets 10 likesShow this thread -
-
Replying to @Profpatsch
I renewed the certificate last month, maybe a caching issue?
2 replies 0 retweets 0 likes
Firefox 75 on latest MacOS here and WFM.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.