Am i not already using it when I Ctrl-Space in IntelliJ?
Why Don't People Use Formal Methods?
11–20 of 232 posts
Re: Why Don't People Use Formal Methods?
#12Back when I did my CS degree, we were taught the "B-method": https://en.wikipedia.org/wiki/B-Method
The course dropped in popularity with students and the university eventually dropped it.
Looking back on it, it really should've been a mandatory course for all software engineering students.
Re: Why Don't People Use Formal Methods?
#13> Why Don't People Use Formal Methods?
Because they're an emerging and unproven technology? Why don't people rewrite everything in Rust? That would surely be a lot more straightforward than adopting the sorts of "formal methods" where you only write a handful of (C-language equivalent) LOC per day, across the software industry! So why doesn't it happen? There's your answer.
Re: Why Don't People Use Formal Methods?
#14I think it goes beyond conservatism for most devs as to why you don't formally specify your design and its mostly rooted in why AGILE is so popular. The sooner you show a finished product, no matter how broken and incomplete, the sooner your client can realize all the things they didn't want they said they did and replace them. If you give them a formal design document it might be ironclad and foolproof but it doesn'…
You are right in general where the cost of failing is not that high, but consider software on flights, a pacemaker or (the best example everyone in FM quotes) a space mission. The cost of a small bug can cost you huge money/lifes. In these cases companies have an incentive to verify their code. Hey you don't have to go to these special cases. Amazon, google, Microsoft all do Formal verification (or have started somew…
But most software is not on flights, pacemakers or space missions (or equivalent).
Re: Why Don't People Use Formal Methods?
#15Does anyone here have any experience using semi-formal methods, like 'cleanroom' techniques? The commentaries I've heard (e.g. [1]) tend to be very enthusiastic, but I don't have enough experience to judge their credibility so I'd love to hear what others have to say on the matter.
Re: Why Don't People Use Formal Methods?
#16Do life dependent code like those in NASA use these type of method to validate their system?
Re: Why Don't People Use Formal Methods?
#17I think it goes beyond conservatism for most devs as to why you don't formally specify your design and its mostly rooted in why AGILE is so popular. The sooner you show a finished product, no matter how broken and incomplete, the sooner your client can realize all the things they didn't want they said they did and replace them. If you give them a formal design document it might be ironclad and foolproof but it doesn'…
I had a meeting with a customer today.
During the previous meeting one of their highest priority feedbacks was "X doesn't look anything like we want it, we want it to look like A,B,C,D...."
In the meantime I put it on the back burner to work on some other customer's requests.
Before today's follow up meeting I realized I hadn't made any changes to X, first thing they said "X looks great, don't change a thing."
I had done nothing, I double checked and nothing had changed in any way.
I suspect they just needed time to use it a bit and then they realized that it was in fact what they had asked for months earlier. Fortunately we were moving that customer into exactly the phase of "no changes, you use it for 6 weeks then tell us what you think".
Re: Why Don't People Use Formal Methods?
#18Earlier quoted context omitted.
You are right in general where the cost of failing is not that high, but consider software on flights, a pacemaker or (the best example everyone in FM quotes) a space mission. The cost of a small bug can cost you huge money/lifes. In these cases companies have an incentive to verify their code. Hey you don't have to go to these special cases. Amazon, google, Microsoft all do Formal verification (or have started somew…
But most software is not on flights, pacemakers or space missions (or equivalent).
Indeed, under those circumstances, yeah formal and semi-formal methods get used.
But since these circumstance aren't common [goto: very eloquent GP].
Re: Why Don't People Use Formal Methods?
#19Even aircraft software doesn't require formal methods. I have a copy of the DO-178C on my laptop. It's mentioned once in the glossary, once in the appendix A, and once in appendix B.
Formal methods would be great, but most people don't have extremely complex state machines where lives depend on it being right.
Re: Why Don't People Use Formal Methods?
#20Earlier quoted context omitted.
You are right in general where the cost of failing is not that high, but consider software on flights, a pacemaker or (the best example everyone in FM quotes) a space mission. The cost of a small bug can cost you huge money/lifes. In these cases companies have an incentive to verify their code. Hey you don't have to go to these special cases. Amazon, google, Microsoft all do Formal verification (or have started somew…
But most software is not on flights, pacemakers or space missions (or equivalent).
It's a cost benefit analysis, if the failure costs you more than verifying it then you will verify it. Since cost of verification is currently high, if you are not losing millions due to failure it doesn't make sense to verify your code.
Look at fuzzing. No one did fuzzing a decade ago. Since fuzzing became cheap (i.e. due to cheap compute and somewhat due to cloud computing) everyone does fuzzing on pieces of code which remotely appear to be critical.
Even testing. When cost of running a program was high people didn't write test cases. They hand checked programs for bugs.