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:
@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.
Also Arc and RwLock and whatnot, but sure.
-
@pie_flavor it seems like you missed a word. Here, let me help you:
Rust parallelism is
MOSTLY
message-based too.
-
@pie_flavor It's not Haskell or TCL or industry standard.
-
-
@Gąska Which is why I said “step towards”.
-
@topspin my point is that it isn't a step towards - it's doing something entirely different.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@topspin my point is that it isn't a step towards - it's doing something entirely different.
And you’re wrong.
Formal verification requires that you specify exactly what the pre- and post-conditions are. And Eiffel enables that. Formal verification also requires automatic static verification of those, which Eiffel doesn’t. But at least you have the contracts written as code, and they’re checked for everything you run, unlike unit tests which are very limited.
-
@topspin 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:
@topspin my point is that it isn't a step towards - it's doing something entirely different.
And you’re wrong.
Formal verification requires that you specify exactly what the pre- and post-conditions are. And Eiffel enables that. Formal verification also requires automatic static verification of those, which Eiffel doesn’t. But at least you have the contracts written as code, and they’re checked for everything you run, unlike unit tests which are very limited.So how's that different compared to
debug_assert!
and friends?
-
@pie_flavor not exactly sure (did I say it’s the only language doing that? It’s pretty old after all), but I’d guess that it’s part of the function signature and that it specifies what kind of thing it’s asserting.
-
@topspin said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Formal verification requires that you specify exactly what the pre- and post-conditions are. And Eiffel enables that.
Is it possible to access those pre- and post-conditions programatically in any other way than executing them as code (anti-cheap-joke: and other than reading original source or processing compiled program instructions)? If not, then it's not really specifying those conditions. It's just writing a subroutine that verifies an unknown set of conditions that the compiler knows nothing about except that this subroutine verifies them. This is on completely different level than, say, Ada's type ranges.
-
@dkf 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:
Doesn't the final seller carry responsibility over its own sales?
In Europe, yes. In the US, often not.
In the U.S., under the UCC, the final seller does carry responsibility. If you buy a defective product from a retailer, you can bring it back to the retailer and demand your money back. The retailer may try to convince you that your only option is to seek a refund from the manufacturer, and it may not be worth your effort to argue with him, but it's not legally true.
-
@boomzilla Yes, but in this case they only needed to have tried their solution in the exact same scenario where the first plane went down.
I.e. going just one step further: "If pilots use this method to shut MCAS down under the known conditions, is the pilot able to use manual trim to stabilize the plane again?"
-
@jinpa Works the same way in the EU.
-
@pie_flavor said in What if we just didn't write the bugs, then we wouldn't have buggy software:
So how's that different compared to
debug_assert!
and friends?It's not hugely different. It's just more systematic about insisting that they're there and about where they belong in the code.
-
@dkf One thing I want from a contract-based language is the ability to dynamically enable or disable checking all those conditions at runtime. And possibly even an algorithm that does it for me.
Example: during debugging, keep them on. For the first N executions of a function in any new computer, keep them on. After that, randomly enable them with 0.1% probability. If there's a crash or exception, re-enable the checks to detect possible extra problems, etc.
Edit: and disable checks entirely if it can prove it's always true, I forgot that case.
-
@anonymous234 that sounds like a lot of overhead. Why not keep them on all the time? I can see that it might not work when the contract computations are extra expensive - but I don't think that's a good contract.
-
@Rhywden said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@boomzilla Yes, but in this case they only needed to have tried their solution in the exact same scenario where the first plane went down.
I.e. going just one step further: "If pilots use this method to shut MCAS down under the known conditions, is the pilot able to use manual trim to stabilize the plane again?"
Yes. The point being that people miss critical cases like that and will continue to miss critical cases like that no matter how well they handle the rest of them.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@anonymous234 that sounds like a lot of overhead.
Eh...JIT happens all over the place doing stuff like this. The extra overhead means diddly for most code.
-
@boomzilla dynamically re-JITing the already JITed code to periodically enable or disable contract checks? That also sounds like overhead. Why not just leave them on all the time?
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@boomzilla dynamically re-JITing the already JITed code to periodically enable or disable contract checks? That also sounds like overhead. Why not just leave them on all the time?
I thought the overhead you were talking about was the monitoring and changing, i.e., re-JITing. As to the rest, I have no idea. This is all theoretical and to make a good judgment I'd have to see some empirical results. I'm just saying that the concept sounds plausible since it seems very similar to some of the stuff that we do already.
-
@Gąska huh? Just include
if thread_rng().gen_ratio(1, 1000) {
in the JITing.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
I can see that it might not work when the contract computations are extra expensive - but I don't think that's a good contract.
Remember: if the compiler can prove that the contract must hold at that point, it can actually elide the code to do the check. Compilers are getting good at this.
-
@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:
@boomzilla dynamically re-JITing the already JITed code to periodically enable or disable contract checks? That also sounds like overhead. Why not just leave them on all the time?
I thought the overhead you were talking about was the monitoring and changing, i.e., re-JITing.
My initial idea was constant checks, like compile in the bytecode that says "if X then runTests()" and the condition is checked every time a function is called. This, re-JITing, and just having everything on all the time all sound like they'd have roughly the same performance impact, and having everything on all the time is a clear winner in bug detection department. Of course it all depends on the specifics of the environment and the checks themselves, but as a rule of thumb, you should almost always go with "all checks all the time", unless performance is a concern, then you should almost always go with "no checks at all".
-
@dkf 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:
I can see that it might not work when the contract computations are extra expensive - but I don't think that's a good contract.
Remember: if the compiler can prove that the contract must hold at that point, it can actually elide the code to do the check. Compilers are getting good at this.
The extra expensive stuff is usually the kind that can never be elided because it involves IO of some kind or other syscalls.
-
@Gąska A common check could be iterating through an entire array checking that every element follows a certain condition (or worse, every combination of elements). That can get expensive pretty fast.
-
@anonymous234 right, if that's the kind of stuff you're checking, then it certainly can be expensive even without IO. You certainly don't want it to happen at runtime all the time.
To be honest, I don't think I'd ever put such a check in postconditions. It's way too much cost for way too little gain. And the other postcondition checks probably cover it anyway. It's certainly something I'd do in unit tests, because performance of unit tests is virtually never a concern.
-
Not to mention, we don't know how internal discussions at Boeing went. I'd be surprised if no one said "huh, guys, this is not a good idea" and been told to shut up.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
The extra expensive stuff is usually the kind that can never be elided because it involves IO of some kind or other syscalls.
I find it hard to believe that using a system call in a function contract descriptor is a good idea.
-
@dkf because it's expensive.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
because it's expensive.
No, because it's poorly characterised.
-
@dkf how so? If I make a function that stores some information in a shared storage available as system service, it makes sense to make sure the information is then accessible as a postcondition.
-
@levicki 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:
@dkf how so? If I make a function that stores some information in a shared storage available as system service, it makes sense to make sure the information is then accessible as a postcondition.
That literally means you just set
FILE_ATTRIBUTE_UNBUFFERED | FILE_ATTRIBUTE_WRITETHROUGH
to everyCreateFile()
callOnly to those where it's actually a postcondition that when I write to those files, the information is immediately accessible for other openers. In other words... only those that already have those flags.
and that you gave up on async I/O if you expect a guarantee of data being written and available upon some
write()
function returnOnly in cases where async I/O has already been given up by design.
not to mention that you cannot even guarantee that it will be accessible because a system might crash after writing or the permissions won't allow access, etc.
If you allow the possibility for that system to crash, it's not postcondition. If you don't allow the possibility for that system to crash (there are valid reasons for it, especially in embedded), there's no reason why you shouldn't crash too.
-
@Zerosquare said in What if we just didn't write the bugs, then we wouldn't have buggy software:
Not to mention, we don't know how internal discussions at Boeing went. I'd be surprised if no one said "huh, guys, this is not a good idea" and been told to shut up.
Right, but let me play : this kind of thing almost certainly a dozen times for every new plane they make. The fact that planes don't fall out of the sky every wednesday, means that their software is already 1000x better than anything we see in our daily lives.
-
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@dkf how so? If I make a function that stores some information in a shared storage available as system service, it makes sense to make sure the information is then accessible as a postcondition.
I think, strictly speaking, the postcondition would be "Write() function has been called once pointing to data that had this content". Whether the file now contains the data or not is the OS' responsibility, and if you know that for sure you'll now have to involve all the hairy file system details (caching, etc.) in your model...
-
@anonymous234 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:
@dkf how so? If I make a function that stores some information in a shared storage available as system service, it makes sense to make sure the information is then accessible as a postcondition.
I think, strictly speaking, the postcondition would be "Write() function has been called once pointing to data that had this content". Whether the file now contains the data or not is the OS' responsibility, and if you know that for sure you'll now have to involve all the hairy file system details (caching, etc.) in your model...
There's a reason I said "shared storage available as system service", not "filesystem". I meant something like RPC manager/local master server, not a bottomless hole you drop things to and not care what happens to them afterwards that files usually are. Though looking how literally everyone thought I'm talking about filesystems, I admit I could've worded it very poorly.