5 ms·

As far as I'm aware, unless your software is Hello World simple, the only way to make sure it's correct is to not write it in the first place. After that point

As far as I'm aware, unless your software is Hello World simple, the only way to make sure it's correct is to not write it in the first place. After that point, everything is a compromise.

mellavora 5y ago
Well, my software is always correct. Sometimes the spec is a bit wrong, like forgetting to be explicit in precisely how the system should crash on a certain unexpected input.
- ChrisMarshallNY 5y ago
  Great answer!
unionpivo 5y ago
> ... Hello World simple End even then only if you stick to English strig hello world. I have had hello worlds fail, in other languages :)
- benttoothpaste 5y ago
  Hello world definitely can fail even in English. It's just that nobody checks to make sure the print operation succeeded.
junon 5y ago
Formalized verification would say otherwise.
- pydry 5y ago
  At its worst, formalized verification is an elaborate and overcomplicated process for converting coding bugs into specification bugs.
  - junon 5y ago
    This is a huge copout and isn't at all correct. It dismisses a bunch of insanely intelligent peoples' life works.
    - odonnellryan 5y ago
      Can't you use this same argument when being critical about any technology, or really anything complex at all? It is some kind of logical fallacy - just because really smart people worked on something and dedicated their lives to it doesn't mean it is good or correct or that it works.
      - junon 5y ago
        The point was more the parent comment was dismissing the work clearly without understanding any of it. They employed a sound byte to disclaim something. You're welcome to go read the prose on the subject. Parent commenter clearly hasn't.
    - pydry 5y ago
      It's a wry observation that I made when I was forced to learn it by those very same researchers who hyped it up as the future of software development 20 years ago. It was sold as the "rolls royce of testing" which I think overstated its capabilities and effectiveness.
      - junon 5y ago
        Okay but things are entirely different than 20 years ago.
- deleted 5y ago
  [deleted]
- mhh__ 5y ago
  Not everyone has a spare 1000 programmer-years to write their script in Coq though. Model checking can be pretty productive relatively speaking, however.
  - junon 5y ago
    Yeah this is unfortunately true. The developer experience aspect needs a lot of work here. I don't disagree. But the assertion that you can't write bug free code is still false, regardless of the amount of effort it takes.
    - odonnellryan 5y ago
      Lots of my bugs are because of unexpected data. I imagine these systems cannot account for that?
      - junon 5y ago
        Of course they can.
        odonnellryan 5y ago
        How?
      - jeffreygoesto 5y ago
        That can be improved if you practice to "switch hats" and try to break your own code in all ways you can think of. That is something worth doing when you review other people's PRs as well. Expect all possible inputs before they hit you. Kind of a human fuzzer.
        odonnellryan 5y ago
        Well, yes this is good advice no matter what, but it doesn't get rid of the bugs!
- adwn 5y ago
  The problem with formal verification is that in practice, many problems can't even be formally specified. Try formally specifying the requirement "the GUI should work as expected" – it's hard enough even to test this, and impossible to formally specify. Of the remaining problems, the complete, formal specification would be larger, more complex, and more bug-ridden than the implementation. "Hey adwn, can you add a button to the GUI so the user can export the current dataset to a CSV file?" Maybe 20-50 lines of code, but a full specification would be a multi-year project – and it would be almost certainly wrong.
  - AnimalMuppet 5y ago
    > The problem with formal verification is that in practice, many problems can't even be formally specified. And even if they can, where does that formal spec come from? Sooner or later, it comes from some informal understanding of what's supposed to happen. Well, how do you check that the formal spec is correct? Because if you can't do that, all formal verification can do is tell you that your program correctly implemented the wrong thing. And I don't think you can do that. First, I don't think you can go from informal to formal by formal means. Second, even if you can, you still can't verify the informal spec. So formal verification can only go so far. I can recall several things that were bugs in the spec. Log4j is the most recent example. Heartbleed I think was a specification bug. Back in the day, a lot of computer viruses were helped on their way by bad ideas in the specification of Microsoft Outlook.
ChrisMarshallNY 5y ago
I write UI and communication software. It is pretty much impossible to write meaningful tests that cover everything. This is especially true, when you mix complex, asynchronous server interactions, with random-access UI. Today, I am fixing a couple of bugs in an app that interacts with three different servers (all asynchronously, but some semi-synchronously. The timing diagram is a bit ... intense), and also allows the user to do things like switch contexts, while some part of the server interaction is still unresolved. I write a bit about my approach to testing, here: https://littlegreenviper.com/miscellany/testing-harness-vs-unit/ https://littlegreenviper.com/miscellany/testing-harness-vs-u...
- monkeyjoe 5y ago
  I started reading through your site a bit. Great content. Wanted to let you know that the "Here is the Doxygen-generated documentation for the BADGER layer" link is broken on this page: https://littlegreenviper.com/miscellany/forensic-design-documentation/ https://littlegreenviper.com/miscellany/forensic-design-docu...
  - ChrisMarshallNY 5y ago
    Hey, thanks! I'll look at that.
commandlinefan 5y ago
You can try, though - and demonstrate that you did. I've seen bugs that would have been trivially caught if the software had been run even one time - so it was clear that the software had never been run even one time.
- ohwellhere 5y ago
  This is my favorite. Doesn't even compile, or crashes immediately, and yet... it's somehow in a PR.
  - klyrs 5y ago
    I've done that. Spend days testing a patch, getting everything just right. Then, as you're doing final touchup, you introduce a syntax error with a wrong keystroke and fail to notice before pushing to the PR branch. But, of course, this is why we use CI.
- gitgrump 5y ago
  I've had "senior engineers" and engineering directors submit PRs that just flat out don't work. Like, I ran a minimum working example and it just... didn't work. I swear to God, some people are actually professionally negligent at this point.

As far as I'm aware, unless your software is Hello World simple, the only way to make sure it's correct is to not write it in the first place. After that point, everything is a compromise.

mellavora 5y ago

Well, my software is always correct. Sometimes the spec is a bit wrong, like forgetting to be explicit in precisely how the system should crash on a certain unexpected input.

ChrisMarshallNY 5y ago
Great answer!

unionpivo 5y ago

> ... Hello World simple End even then only if you stick to English strig hello world. I have had hello worlds fail, in other languages :)

benttoothpaste 5y ago
Hello world definitely can fail even in English. It's just that nobody checks to make sure the print operation succeeded.

junon 5y ago

Formalized verification would say otherwise.

pydry 5y ago
At its worst, formalized verification is an elaborate and overcomplicated process for converting coding bugs into specification bugs.
- junon 5y ago
  This is a huge copout and isn't at all correct. It dismisses a bunch of insanely intelligent peoples' life works.
  - odonnellryan 5y ago
    Can't you use this same argument when being critical about any technology, or really anything complex at all? It is some kind of logical fallacy - just because really smart people worked on something and dedicated their lives to it doesn't mean it is good or correct or that it works.
    - junon 5y ago
      The point was more the parent comment was dismissing the work clearly without understanding any of it. They employed a sound byte to disclaim something. You're welcome to go read the prose on the subject. Parent commenter clearly hasn't.
  - pydry 5y ago
    It's a wry observation that I made when I was forced to learn it by those very same researchers who hyped it up as the future of software development 20 years ago. It was sold as the "rolls royce of testing" which I think overstated its capabilities and effectiveness.
    - junon 5y ago
      Okay but things are entirely different than 20 years ago.
deleted 5y ago
[deleted]
mhh__ 5y ago
Not everyone has a spare 1000 programmer-years to write their script in Coq though. Model checking can be pretty productive relatively speaking, however.
- junon 5y ago
  Yeah this is unfortunately true. The developer experience aspect needs a lot of work here. I don't disagree. But the assertion that you can't write bug free code is still false, regardless of the amount of effort it takes.
  - odonnellryan 5y ago
    Lots of my bugs are because of unexpected data. I imagine these systems cannot account for that?
    - junon 5y ago
      Of course they can.
      - odonnellryan 5y ago
        How?
    - jeffreygoesto 5y ago
      That can be improved if you practice to "switch hats" and try to break your own code in all ways you can think of. That is something worth doing when you review other people's PRs as well. Expect all possible inputs before they hit you. Kind of a human fuzzer.
      - odonnellryan 5y ago
        Well, yes this is good advice no matter what, but it doesn't get rid of the bugs!
adwn 5y ago
The problem with formal verification is that in practice, many problems can't even be formally specified. Try formally specifying the requirement "the GUI should work as expected" – it's hard enough even to test this, and impossible to formally specify. Of the remaining problems, the complete, formal specification would be larger, more complex, and more bug-ridden than the implementation. "Hey adwn, can you add a button to the GUI so the user can export the current dataset to a CSV file?" Maybe 20-50 lines of code, but a full specification would be a multi-year project – and it would be almost certainly wrong.
- AnimalMuppet 5y ago
  > The problem with formal verification is that in practice, many problems can't even be formally specified. And even if they can, where does that formal spec come from? Sooner or later, it comes from some informal understanding of what's supposed to happen. Well, how do you check that the formal spec is correct? Because if you can't do that, all formal verification can do is tell you that your program correctly implemented the wrong thing. And I don't think you can do that. First, I don't think you can go from informal to formal by formal means. Second, even if you can, you still can't verify the informal spec. So formal verification can only go so far. I can recall several things that were bugs in the spec. Log4j is the most recent example. Heartbleed I think was a specification bug. Back in the day, a lot of computer viruses were helped on their way by bad ideas in the specification of Microsoft Outlook.

ChrisMarshallNY 5y ago

I write UI and communication software. It is pretty much impossible to write meaningful tests that cover everything. This is especially true, when you mix complex, asynchronous server interactions, with random-access UI. Today, I am fixing a couple of bugs in an app that interacts with three different servers (all asynchronously, but some semi-synchronously. The timing diagram is a bit ... intense), and also allows the user to do things like switch contexts, while some part of the server interaction is still unresolved. I write a bit about my approach to testing, here: https://littlegreenviper.com/miscellany/testing-harness-vs-unit/ https://littlegreenviper.com/miscellany/testing-harness-vs-u...

monkeyjoe 5y ago
I started reading through your site a bit. Great content. Wanted to let you know that the "Here is the Doxygen-generated documentation for the BADGER layer" link is broken on this page: https://littlegreenviper.com/miscellany/forensic-design-documentation/ https://littlegreenviper.com/miscellany/forensic-design-docu...
- ChrisMarshallNY 5y ago
  Hey, thanks! I'll look at that.

commandlinefan 5y ago

You can try, though - and demonstrate that you did. I've seen bugs that would have been trivially caught if the software had been run even one time - so it was clear that the software had never been run even one time.

ohwellhere 5y ago
This is my favorite. Doesn't even compile, or crashes immediately, and yet... it's somehow in a PR.
- klyrs 5y ago
  I've done that. Spend days testing a patch, getting everything just right. Then, as you're doing final touchup, you introduce a syntax error with a wrong keystroke and fail to notice before pushing to the PR branch. But, of course, this is why we use CI.
gitgrump 5y ago
I've had "senior engineers" and engineering directors submit PRs that just flat out don't work. Like, I ran a minimum working example and it just... didn't work. I swear to God, some people are actually professionally negligent at this point.