4 ms·

> The only thing that matters to how software works for an end user is its boundary. You're ignoring the fact that tests aren't only to validate "end user func

> The only thing that matters to how software works for an end user is its boundary. You're ignoring the fact that tests aren't only to validate "end user functionality". They're also there to make life easier for the developer; to make both initial development and maintenance easier. If I need a custom sort algorithm for my product, I'm going to write unit tests for it's implementation. I'm also going write functional tests to make sure the end user is seeing things sorted. However, those tests serve different purposes. The unit tests allow me to write clean, simple tests that show exactly what the implementation is supposed to be doing for different inputs. That allows me to change the implementation of the sorting algorithm later and worry less about breaking the functionality. The functional tests are (generally) not going to be as clean and obvious, nor cover every possible partition of inputs that the implementation could get.

sago 11y ago
> You're ignoring the fact that tests aren't only to validate "end user functionality". Erm, no, that was my entire point!
- RHSeeger 11y ago
  Wow... um... you're right. I was flitting around and dealing with external communication at the same time; you have my apologies. I think my points align pretty well with what you were saying instead of against it.
  - sago 11y ago
    Thanks for the response, it's fun to read someone strongly disagreeing while saying what you think. slightly baffling, but fun ;)
agentultra 11y ago
> If I need a custom sort algorithm for my product, I'm going to write unit tests for it's implementation. I would start with writing an assertion about the end state of the sort. Then using syntactic substitution of the predicate calculi derive the program by assertions. I'd then have a specification of the algorithm as a mathematical model from which I can check every possible execution for the entire domain on the sort. If I'm so inclined I would have a good basis for a proof. The unit tests then become assertions on the implementation and don't have to verify correctness. It would be awesome though if I could just generate the code directly from the specification!
- jkaptur 11y ago
  You would? Can you demonstrate how that would work for, say, a sort algorithm with a tunable "fuzziness" parameter? Informally, after the algorithm is complete, each element is within k indices of where it would be after a traditional sort. So k=0 could just be quicksort, but as k approaches the length of the input we have to do less and less work. It's easy to dream up algorithms and traditional unit tests for this (and easy to see how the large input space makes the approach suboptimal). I'd love to see how your approach would work.
- MichaelBurge 11y ago
  Would you actually do this, or do you just like to imagine a world where people do this? I'm familiar with Coq and Prolog(one of which I think you're hinting at), but I'd reach for Perl or C over either one if I needed to write a trading program or generate a statement from my accounting software or something.
  - agentultra 11y ago
    I learning to use these techniques in my everyday work (cloud software). I think of it like this: nobody is going to care if I screw up the script to balance my accounts. If I write some software that messes up the balance of everyone's account in some bank then someone is going to care. I don't think formal methods and rigor are the sole domain of government institutions, avionics control software, and industrial robotics. The public relies on the cloud and the applications that run on it and they have no recourse if their data is exposed or disappears. Imagine if instead of crossing over a bridge you were stopped at a booth and asked to sign a wager stating that nobody is liable if the bridge collapses underneath you while you cross it. Rich or poor, regardless of how much you pay in taxes, you should be able to rely on that bridge being built to the highest standards we know how and someone should be liable if it falls down. You can rely on this in real life. Why do we not have this for software? I'm not saying I write all of my software using formal methods and rigorous proofs. It's often good enough to sketch my idea on the back of a napkin when I'm building a tool shed. But nobody built a sky-scraper without doing a little math and being fairly rigorous in their thinking.

sago 11y ago

> You're ignoring the fact that tests aren't only to validate "end user functionality". Erm, no, that was my entire point!

RHSeeger 11y ago
Wow... um... you're right. I was flitting around and dealing with external communication at the same time; you have my apologies. I think my points align pretty well with what you were saying instead of against it.
- sago 11y ago
  Thanks for the response, it's fun to read someone strongly disagreeing while saying what you think. slightly baffling, but fun ;)

agentultra 11y ago

> If I need a custom sort algorithm for my product, I'm going to write unit tests for it's implementation. I would start with writing an assertion about the end state of the sort. Then using syntactic substitution of the predicate calculi derive the program by assertions. I'd then have a specification of the algorithm as a mathematical model from which I can check every possible execution for the entire domain on the sort. If I'm so inclined I would have a good basis for a proof. The unit tests then become assertions on the implementation and don't have to verify correctness. It would be awesome though if I could just generate the code directly from the specification!

jkaptur 11y ago
You would? Can you demonstrate how that would work for, say, a sort algorithm with a tunable "fuzziness" parameter? Informally, after the algorithm is complete, each element is within k indices of where it would be after a traditional sort. So k=0 could just be quicksort, but as k approaches the length of the input we have to do less and less work. It's easy to dream up algorithms and traditional unit tests for this (and easy to see how the large input space makes the approach suboptimal). I'd love to see how your approach would work.
MichaelBurge 11y ago
Would you actually do this, or do you just like to imagine a world where people do this? I'm familiar with Coq and Prolog(one of which I think you're hinting at), but I'd reach for Perl or C over either one if I needed to write a trading program or generate a statement from my accounting software or something.
- agentultra 11y ago
  I learning to use these techniques in my everyday work (cloud software). I think of it like this: nobody is going to care if I screw up the script to balance my accounts. If I write some software that messes up the balance of everyone's account in some bank then someone is going to care. I don't think formal methods and rigor are the sole domain of government institutions, avionics control software, and industrial robotics. The public relies on the cloud and the applications that run on it and they have no recourse if their data is exposed or disappears. Imagine if instead of crossing over a bridge you were stopped at a booth and asked to sign a wager stating that nobody is liable if the bridge collapses underneath you while you cross it. Rich or poor, regardless of how much you pay in taxes, you should be able to rely on that bridge being built to the highest standards we know how and someone should be liable if it falls down. You can rely on this in real life. Why do we not have this for software? I'm not saying I write all of my software using formal methods and rigorous proofs. It's often good enough to sketch my idea on the back of a napkin when I'm building a tool shed. But nobody built a sky-scraper without doing a little math and being fairly rigorous in their thinking.