What if we just didn't write the bugs, then we wouldn't have buggy software
-
@Gąska according to the guy writing the article (Senior Lecturer at dunno which British university, not a guy picked up from a street) not enough is done. I choose to entertain his opinion. And anyway why do the developers rapidly iterate if not to provide more features and more stuff to users?
-
@admiral_p said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska according to the guy writing the article (Senior Lecturer at dunno which British university, not a guy picked up from a street) not enough is done. I choose to entertain his opinion.
That guy wasn't talking about design. At all. He was talking about formal verification only. And so was Dijkstra in that quote.
And anyway why do the developers rapidly iterate if not to provide more features and more stuff to users?
To spend less time fixing bugs. Because the faster you detect bugs, the less time you spend fixing them. And the shorter iterations, the earlier you can start testing, so the earlier you find the bugs.
-
@Gąska formal verification is, in my view, a part of the design process. The idea is that you haven't designed anything if you haven't proved it to be correct. You're arguing semantics here.
And why do you have to rapidly iterate if not because you had to introduce features quickly? (And introduce bugs ultimately).
Maybe rapid iteration wasn't the term I was looking for. Rapid pace of development, if you prefer.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
You said that if you were given perfect spec, you'd never make any error in code.
I didn't say I'd get it right the first time and wouldn't need to run tests or do bug fixing. I said that given complete specs, I could write code that implemented them. I didn't think I needed to qualify that with "eventually", since the point I was making was that when your spec is a moving target, bug free code is impossible.
Basically, specs define behaviors. Given a finite set of behaviors, I can write tests that cover those behaviors. If my code can pass the tests, even without formal verification I can have sufficient confidence that my code implements the spec to the degree that the spec defines anything. It's not formal verification but it's close enough. Formal verification is better, but the requirement for them is such that it's not practical, and if you could meet their requirements, we have plenty of other tools that would also get us nearly there.
And then you get to the part where even if you pass the formal verification, the program could still be "buggy" because the spec required the wrong thing. And "bug free" doesn't mean "adheres to the spec", which is what formal verification guarantees, but "does what the people using it need it and expect it to do". Which basically means that bugs are subjective, and formal verification is objective, so even with perfect formal verification you can't guarantee that a program is bug free.
-
@admiral_p said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska formal verification is, in my view, a part of the design process. The idea is that you haven't designed anything if you haven't proved it to be correct.
You seem to have a mistaken idea what formal verification means in this context. It's not about verifying your specification is correct. It's about verifying your implementation conforms specification. It's development process, not design process. It's basically type checking on steroids.
You're arguing semantics here.
I never understood the point of that saying. Isn't semantics - the meaning of what we say, as opposed to the form of how we say it - the only part worth arguing about?
And why do you have to rapidly iterate to fix bugs if not because you had to introduce features quickly?
You can make the same argument about literally everything. Why do you have to do more upfront design if not because you have to introduce features quickly?
-
@Kian everything you say is true (well, mostly true, but whatever). It's just that it sounded like you think there's no place for formal verification in software development at all, because a good spec is all that a developer needs to avoid bugs.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@admiral_p said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska formal verification is, in my view, a part of the design process. The idea is that you haven't designed anything if you haven't proved it to be correct.
You seem to have a mistaken idea what formal verification means in this context. It's not about verifying your specification is correct. It's about verifying your implementation conforms specification. It's development process, not design process. It's basically type checking on steroids.
If you design an electronic circuit assuming ideal components with ideal behaviour, and then you can't use those ideal components (because they don't exist), is it a real design? Or is it just a back-of-napkin mockup? What's implementation? Is implementation the code or the end result?
You're arguing semantics here.
I never understood the point of that saying. Isn't semantics - the meaning of what we say, as opposed to the form of how we say it - the only part worth arguing about?
Yeah, it should be "morphology", probably.
And why do you have to rapidly iterate to fix bugs if not because you had to introduce features quickly?
You can make the same argument about literally everything. Why do you have to do more upfront design if not because you have to introduce features quickly?
Maybe you design (or develop, if you will) more to implement fewer features better.
-
@admiral_p said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@admiral_p said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska formal verification is, in my view, a part of the design process. The idea is that you haven't designed anything if you haven't proved it to be correct.
You seem to have a mistaken idea what formal verification means in this context. It's not about verifying your specification is correct. It's about verifying your implementation conforms specification. It's development process, not design process. It's basically type checking on steroids.
If you design an electronic circuit assuming ideal components with ideal behaviour, and then you can't use those ideal components (because they don't exist), is it a real design?
Oh, so we're talking about hardware design now? Can we finish the discussion about software design first? Because, you know, we've already started that one, and it's a completely different topic from software design.
What's implementation? Is implementation the code or the end result?
And why do you have to rapidly iterate to fix bugs if not because you had to introduce features quickly?
You can make the same argument about literally everything. Why do you have to do more upfront design if not because you have to introduce features quickly?
Maybe you design (or develop, if you will) more to implement fewer features better.
No, you don't. No one ever designs with the goal of making less features overall in mind. Upfront design is done so the overall development process goes faster, freeing up time for designing and developing more features. Exactly like rapid iterations. Alternatively, upfront design is done to develop the same set of features in shorter time. Exactly like rapid iterations.
You seem to be confusing software design with project planning. Design is only about how features are to be made. What features are to be made in the first place, and in what order, is covered entirely by project planning.
-
@Gąska my point is that software would probably benefit if it were approached as if it were hardware. Software has advantages to hardware. Maybe developers should act (in part, of course) as if those advantages do not exist. If you were instead saying that hardware components and materials are a bad analogy for code, well, are they really? Depending on the language (and the compiler too, I suppose, and the architecture too) behaviour is not necessarily ideal or the expected one. Then the fact that the stuff I'm talking about "goes here, not there" is immaterial. Yes, I'm probably talking about the process, not the development per se.
-
@admiral_p said in What if we just didn't write the bugs, then we wouldn't have buggy software:
There is no need for such speed
Tell that to our "stakeholders". It's a very competitive market out there
-
@dkf said in What if we just didn't write the bugs, then we wouldn't have buggy software:
We can quite easily produce correct software from mathematically-defined specifications
Really? We can?
Maybe for simple stuff.
Not for anything of value.
That concept falls apart once concurrency is involved.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Zerosquare said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Yes, indeed. But how do you know that those tools themselves are correct?
By performing formal verification on the formal verification software. You can, for example, use the formal verification software you're formally verifying to verify that. Also, traditional testing. Also, manual verification. Of course you will never have 100% certainty (if you account for the possibility of every single human ever attempting to formally verify software, making an error of some sort that results in false positive), but 99.999% is totally within grasp.
Heh...and I'll bet the Boeing 737 MAX stuff would have passed! Because the problem was at a higher level (as I understand it). And even if that's not the case, it's still a reality. We've had this discussion before. Verification isn't enough. You have to validate it, too. That is, does it do what we really want it to do?
And how do you decide it's what you really want it to do? This sort of thing comes up all the time. Customers start complaining about a bug and it turns out the software is doing exactly what they'd previously asked for. Except they hadn't thought about this particular case.
So even if you have some system that flawlessly translates the formal logic into code (hey...this sounds a lot like compilers that we all use every day!) you're still going to have problems developing that stuff.
Which isn't to say that we shouldn't try to improve (hi @blakeyrat!) but that we shouldn't pretend there's some magic wand in our possession that we just need to start using.
-
@anonymous234 said in What if we just didn't write the bugs, then we wouldn't have buggy software:
I'm not going to say "just formally verify everything lol", but I do think programming needs to get a lot more formal.
MONADS!
/HaskellFanatic
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Kian said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Kian said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Hell, give me those two things and I would write bug free code even without formal verification methods.
Are you a pope? Because it looks like you believe in your own infallibility.
I don't have a cool hat, but I'm just saying that given an impossible requirement I can produce an impossible outcome, which is the same thing that proponents of formal verification do.
You said that if you were given perfect spec, you'd never make any error in code. Which is either extreme arrogance or serious misunderstanding. People will always make errors. That's human nature.
Holy fucking shit. IT WAS A JOKE ABOUT HOW NO ONE CAN MAKE UP THEIR MIND OR EVEN GET REQUIREMENTS CORRECT.
-
@boomzilla said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Zerosquare said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Yes, indeed. But how do you know that those tools themselves are correct?
By performing formal verification on the formal verification software. You can, for example, use the formal verification software you're formally verifying to verify that. Also, traditional testing. Also, manual verification. Of course you will never have 100% certainty (if you account for the possibility of every single human ever attempting to formally verify software, making an error of some sort that results in false positive), but 99.999% is totally within grasp.
Heh...and I'll bet the Boeing 737 MAX stuff would have passed!
Of course it would pass. Everything was working as intended. It's those cheapskate airlines that are at fault for not buying the optional fuckup detector that would have saved all those lives.
We've had this discussion before. Verification isn't enough. You have to validate it, too. That is, does it do what we really want it to do?
Sure. I'm just against this "formal verification isn't perfect therefore it's not worth it" attitude.
-
@boomzilla A bit ironic considering the answer to that was "people will always make errors".
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@admiral_p so that sentence should read "the users spoiled by rapid iteration"? TDEMSYR. Users don't benefit from rapid iteration. In most cases, they're not even aware of rapid iteration - because why would they? It's an internal matter of the development team. The user has neither any knowledge nor any interest in knowing those processes.
It's not a given, because crap can always be produced, but they often benefit from giving developers quicker feedback so that, for instance, a design flaw doesn't propagate to every part of a system instead of being fixed early. They might get features more quickly.
Obviously, things can go wrong and the process could be a disaster from all angles, but that's life and doesn't negate the fact that users often very much do benefit from rapid iteration.
-
@boomzilla said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Kian said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Kian said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Hell, give me those two things and I would write bug free code even without formal verification methods.
Are you a pope? Because it looks like you believe in your own infallibility.
I don't have a cool hat, but I'm just saying that given an impossible requirement I can produce an impossible outcome, which is the same thing that proponents of formal verification do.
You said that if you were given perfect spec, you'd never make any error in code. Which is either extreme arrogance or serious misunderstanding. People will always make errors. That's human nature.
Holy fucking shit. IT WAS A JOKE ABOUT HOW NO ONE CAN MAKE UP THEIR MIND OR EVEN GET REQUIREMENTS CORRECT.
And what do you think the pope line was? Exhaust filter?
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@boomzilla said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Kian said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Kian said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Hell, give me those two things and I would write bug free code even without formal verification methods.
Are you a pope? Because it looks like you believe in your own infallibility.
I don't have a cool hat, but I'm just saying that given an impossible requirement I can produce an impossible outcome, which is the same thing that proponents of formal verification do.
You said that if you were given perfect spec, you'd never make any error in code. Which is either extreme arrogance or serious misunderstanding. People will always make errors. That's human nature.
Holy fucking shit. IT WAS A JOKE ABOUT HOW NO ONE CAN MAKE UP THEIR MIND OR EVEN GET REQUIREMENTS CORRECT.
And what do you think the pope line was? Exhaust filter?
More like the air rushing out through the exhaust.
-
@boomzilla biologically speaking, that's pretty accurate. Complete with greenhouse gases!
-
@boomzilla said in What if we just didn't write the bugs, then we wouldn't have buggy software:
So even if you have some system that flawlessly translates the formal logic into code (hey...this sounds a lot like compilers that we all use every day!) you're still going to have problems developing that stuff.
Well yeah. All this concept is doing is pushing it back one step and allowing us to translate more abstract concepts into code, instead of symbols and semantics.
But, as I said, pretend something like this existed as a tool, it would maybe drag boxes and arrows around representing input => output, where => is the function. If you have that picture in your head, you can see it doesn't handle cases of concurrency where things can interact out of order. Every function would have to lock everything it touched. Logically it would function, but you'd find out you could end up taking massive performance hits, because this is only ensuring it performs the logic correctly, not efficiently.
Once you realize that, then you devolve back to ye old triangle of cost/speed/robust, the very reason WE have a JOB!
Even an A.I. would have trouble solving that problem, because it can't assign values to those requirements. That would require human input.
-
@admiral_p said in What if we just didn't write the bugs, then we wouldn't have buggy software:
my point is that software would probably benefit if it were approached as if it were hardware.
Good luck reversing the trend, because hardware is increasingly approached as if it were software.
"Don't worry about the hardware being buggy, the firmware guy will figure out a workaround"
(also works with "firmware / driver", "driver / software", and "software / user". You could call it the "solving your problems by pushing them up" strategy.)
-
@xaade said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@boomzilla said in What if we just didn't write the bugs, then we wouldn't have buggy software:
So even if you have some system that flawlessly translates the formal logic into code (hey...this sounds a lot like compilers that we all use every day!) you're still going to have problems developing that stuff.
Well yeah. All this concept is doing is pushing it back one step and allowing us to translate more abstract concepts into code, instead of symbols and semantics.
But, as I said, pretend something like this existed as a tool, it would maybe drag boxes and arrows around representing input => output, where => is the function. If you have that picture in your head, you can see it doesn't handle cases of concurrency where things can interact out of order. Every function would have to lock everything it touched. Logically it would function, but you'd find out you could end up taking massive performance hits, because this is only ensuring it performs the logic correctly, not efficiently.
Once you realize that, then you devolve back to ye old triangle of cost/speed/robust, the very reason WE have a JOB!
Even an A.I. would have trouble solving that problem, because it can't assign values to those requirements. That would require human input.
I concur that it’s just moving the problem one level, but the concurrency part isn’t insurmountable. It only makes it a bit harder, not impossible. There a reasoning systems that handle that.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Of course it would pass. Everything was working as intended. It's those cheapskate airlines that are at fault for not buying the optional fuckup detector that would have saved all those lives.
Those items shouldn't be optional. The number of crashes shows their base model isn't safe enough.
-
@sockpuppet7 so petition your government to make them not optional.
-
@Kian said in What if we just didn't write the bugs, then we wouldn't have buggy software:
And "bug free" doesn't mean "adheres to the spec",
It officially did at one former employer. If the product met the spec, it was "bug free." If the product didn't meet the actual requirements because the spec was wrong, that was a different problem. Of course, that didn't matter to the customer, but internally, it mattered when it came to assigning blame and determining who got bonuses and who didn't. Just kidding about the last part; if it didn't work, nobody got bonuses, regardless of who was to blame.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@sockpuppet7 so petition your government to make them not optional.
They're already grounded world wide, so I guess it's too late for that.
-
@HardwareGeek: You... you mean that this kind of employers actually exists?!
-
@Zerosquare Be careful what you ask for. There's a Lounge thread about (mostly) that employer.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@ben_lubar said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Not even drunk cats?
Cats getting drunk was not the bug
the bug was that the game mishandled portions of alcohol smaller than 1 unit
-
@Kian said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Basically, specs define behaviors. Given a finite set of behaviors, I can write tests that cover those behaviors. If my code can pass the tests, even without formal verification I can have sufficient confidence that my code implements the spec to the degree that the spec defines anything. It's not formal verification but it's close enough. Formal verification is better, but the requirement for them is such that it's not practical, and if you could meet their requirements, we have plenty of other tools that would also get us nearly there.
If you're actually seriously into doing that right, you can think of the spec as determining what the tests of that spec should be. The effort to write tests to cover the space of a spec without actually working from a spec is usually substantially larger than the effort to create a spec that you can (semi-)automatically derive both tests and code from.
Or at least that's how it was being reported in the literature 20–25 years ago. (I left that field of CS for budgetary reasons.) So far as I can tell, a lot of the research in that area since has been on taking those techniques and integrating them into more standard tools such as optimizing compilers and static analysis systems.
-
What is a spec but the program itself in an annoying to parse language?
-
@xaade said in What if we just didn't write the bugs, then we wouldn't have buggy software:
That concept falls apart once concurrency is involved.
No, you're just using the wrong models.
Shared modifiable memory concurrency is a total bitch to show the correctness of. That's because it is stupid hard to get right, and has a whole lot of problems. Oh yeah, it shows up in the specification and proof layers too. Maybe that's a sign that we should be shunning shared modifiable memory concurrency as an industry?
-
@sockpuppet7 said in What if we just didn't write the bugs, then we wouldn't have buggy software:
They're already grounded world wide, so I guess it's too late for that.
If they're already grounded, a good lightning strike will deal with the problem just fine.
-
@dkf Or maybe it's just a sign that you're doing it wrong. Have you tried Rust's model?
-
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Have you tried Rust's model?
Have you tried Erlang's model?
-
@ben_lubar said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@ben_lubar said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Not even drunk cats?
Cats getting drunk was not the bug
the bug was that the game mishandled portions of alcohol smaller than 1 unit
Alternative take: the cats were mishandling alcohol...
-
@sockpuppet7 sounds like a happy ending!
-
@dkf said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Have you tried Rust's model?
Have you tried Erlang's model?
Eiffel tried to integrate design-by-contract and pre- and post-conditions everywhere, which seems to be a step towards "formal verification for everything".
-
@dkf I have. I was talking about alternative models of shared mutable state. I recall in an earlier version of the Rust Book (it's not there anymore AFAICT), it said that while most languages try to solve the mutable part, Rust tries to solve the shared part. And as a result, in Rust it's impossible to create thread unsafety without the use of unsafe code.
-
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
while most languages try to solve the mutable part, Rust tries to solve the shared part
All the sane models of parallel communications are message-based anyway. And you're shilling Rust so your arguments default to invalid.
-
@dkf said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
while most languages try to solve the mutable part, Rust tries to solve the shared part
All the sane models of parallel communications are message-based anyway.
Because they're implemented in languages that aren't Rust.
And you're shilling Rust so your arguments default to invalid.
Hmm?
-
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
I don't think my eyes are physically capable of rolling any harder.
How to Write Flawless Software Code Using Formal Methods
Strong software engineering, or more usually formal methods, is a methodology that uses mathematics to ensure error-free programming.
Um, let me reiterate the URL: https://ponderwall.com/index.php/2019/04/04/flaw-free-software-possible-math/
Yup. PHP!
So yeah, why don't we?
-
Indeed. There are all sorts of organisational tools we could use to improve our software quality. It's just not profitable to do so.
That's why most places I've worked at use client-driven-development.
-
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
I don't think my eyes are physically capable of rolling any harder.
Do more stretches.
-
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@dkf said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
while most languages try to solve the mutable part, Rust tries to solve the shared part
All the sane models of parallel communications are message-based anyway.
Because they're implemented in languages that aren't Rust.
Rust parallelism is mostly message-based too. And async/await model is also more akin to message passing than shared memory or other paradigms.
-
@topspin said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@dkf said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Have you tried Rust's model?
Have you tried Erlang's model?
Eiffel tried to integrate design-by-contract and pre- and post-conditions everywhere, which seems to be a step towards "formal verification for everything".
Well, if they were some kind of compile time construct that verified that all callers always fullfill all callees' preconditions, then yes. But if it's like the D model of additional runtime checks, and it looks like it is, then it's basically just additional unit tests, and so entirely different from formal verification.
-
@HardwareGeek said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Zerosquare Be careful what you ask for. There's a Lounge thread about (mostly) that employer.
You piqued my curiosity.
I've applied for Lounge access... let's see how this goes.
-
@Zerosquare Lounge access is (mostly) harmless. Applying for Garage access, OTOH, would indicate questionable sanity (even more than being on TDWTF in the first place).
-
@HardwareGeek said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Applying for Garage access, OTOH, would indicate questionable sanity (even more than being on TDWTF in the first place).
Damn, foiled again.
Software implementation - Wikipedia
Ben Lubar (any pronouns) (@ben@lubar.me)
