StilgherrianHas anyone thought about shipping software that doesn’t contain bugs?
oxy ::openbsd:: ::freebsd:: ::runbsd:: @stilgherrian but then you'd never call
Elissa@stilgherrian I tried it once but it's just too much FUN getting bug reports constantly to want to change things up.
@vampiress That’s true. I wouldn’t want people to get bored.
Bakunin Boys@stilgherrian @vampiress literally the software dev process is: let me build this thing. Ah bugger there's a bug let me fix it. Well while I'm here may as well add a feature. Ah shit there's a bug in that feature. Better fix it... while I'm here...
bignoseThe trouble we always encounter is, people *also* want the software to *do* something.
No one has figured out how to make software that always does the right thing, never does the wrong thing, and is still useful enough that people want it.
Zimmie@bignose @stilgherrian There’s always formal verification, which proves the software does everything in the specification and nothing which isn’t in the specification. At that point, the specification can have issues or limitations, but those aren’t really software bugs.
@bob_zim, I would bet money that no system which does something of interest to @stilgherrian has been formally verified to the complete degree you say.
Which is why my description includes the requirement that the software does something people are interested in. Yes, there might exist formally-verified systems with no detectable bugs; but likely that doesn't describe any system we directly use.
David@bignose @bob_zim @stilgherrian though it sounds like curl is pretty dang close! (To being bug/vulnerability-free, and ubiquitously used)
Also assumes that the verification/validation process is flawlessly designed and executed to test all positive cases and all possible negative cases, and I’m gonna hazard a guess that that’s happened only on a handful of systems in the history of the world.
@shieldsy05 @bignose @stilgherrian The verification process involves building a mathematical proof that the software has all of the specified behaviors and has no undefined behaviors. It’s concrete proof of exact match. Writing a sufficiently detailed specification is difficult, of course, but there are tools to help.
It’s mostly worthwhile in the embedded space, industrial process control, and in situations where the hardware is exceptionally difficult to access to update (e.g, satellites). These things are widely deployed, though. This message definitely goes through at least four formally-verified OS kernels on its way to you.
@bob_zim @bignose @stilgherrian that’s fair. A whole lot of use cases I haven’t considered/had knowledge of. My experience is mostly in end-user software in an environment that is only just starting to regulate the computer systems used.
@shieldsy05 @bob_zim @bignose I can’t help but think you’ve all been taking this way too seriously. :)
Don't pretend @stilgherrian that you are unfamiliar with the joy of taking a joke too seriously
@bignose @stilgherrian seL4 is formally verified, and it’s extremely widely used. Several other operating systems are, too. Big chunks of the OS used by Qualcomm modems (so, present in ~95% of smartphones sold in the last year) are formally verified.
David Chisnall (*Now with 50% more sarcasm!*)@bob_zim @bignose @stilgherrian
seL4 is formally verified and went almost 24 hours between being open sourced and the first security vulnerability being reported. That one was because the verification didn't cover all of the code, but seL4's verification was also done against a quiet simplified model of an MMU, so there may be other soundness issues.
My favourite verification story is when some colleagues adopted EverCrypt in a previous job. EverCrypt is verified against a bunch of properties (including constant time execution). It is also proven to be memory safe. They expressed temporal safety as a property that no object is accessed after it was freed. It turned out that the codebase complied with this trivially: it never freed memory.
Oh, and the proofs treat as axiomatic that the C code calling the APIs has no memory safety bugs.
vrek@david_chisnall @bob_zim @bignose @stilgherrian my favorite example I've personally seen was requirements stated "operator shall be able to log into system with company assigned username and password". When you started the application there was a log in prompt for username and password. Problem was the requirements never stated that those should be verified as accurate. Sure login with your credentials... Or just smash your head on the keyboard... Same result
Cycling Stu@stilgherrian Error redo from start, needs more ants
Adam Kent@stilgherrian Not in fashion. Ship more code faster is.
Jason Tubnor 🇦🇺@stilgherrian I’m sure my “hello world” application has zero bugs but it has yet to undergo fuzzing or mythos. Wish me luck!
@tubsta May good fortune go with you.
Rob@stilgherrian all software which is anything other than trivial contains bugs.
The best you can do is have a well thought out and extensive testing regime to catch the majority of them.
But even test code itself will contain bugs too.
Accept you own limitations and organise around them.
The best you can do is have a well thought out and extensive testing regime to catch the majority of them.
But even test code itself will contain bugs too.
Accept you own limitations and organise around them.
The Orange Theme@stilgherrian And put myself out of a job?
Willem Janssen@stilgherrian Sure! First I need to write a better editor. Ooh, and a better language. Oh, and a universe with math that doesn’t have the halting problem…
I’m pondering step 2 and 3 atm.
I’m pondering step 2 and 3 atm.
Just a trash panda 🦝@stilgherrian Not for some decades. 🫠
@trashpanda It’s funny because it’s true. :)