• Post Reply Bookmark Topic Watch Topic
  • New Topic
programming forums Java Mobile Certification Databases Caching Books Engineering Micro Controllers OS Languages Paradigms IDEs Build Tools Frameworks Application Servers Open Source This Site Careers Other Pie Elite all forums
this forum made possible by our volunteer staff, including ...
Marshals:
  • Campbell Ritchie
  • Paul Clapham
  • Ron McLeod
  • Tim Cooke
  • Junilu Lacar
Sheriffs:
  • Rob Spoor
  • Devaka Cooray
  • Jeanne Boyarsky
Saloon Keepers:
  • Jesse Silverman
  • Stephan van Hulst
  • Tim Moores
  • Carey Brown
  • Tim Holloway
Bartenders:
  • Jj Roberts
  • Al Hobbs
  • Piet Souris

Test Driven Development is technically impossible

 
lowercase baba
Posts: 13013
66
Chrome Java Linux
  • Likes 1
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
Note:  This is not a serious post, hence it being in MD

Sooo...test driven development.  it's a thing.  The idea being, you write tests first, then write your code such that it passes the tests.  then you write more tests, update your code to pass those - and still pass the original, etc.

But....The tests are written in java.  Which means they are java code.  So you should write tests for that code first...to test the tests.  But THOSE tests are in java...So really, you can never get started, because any tests you write need to have tests for them written first.

It's tests all the way up!!!
 
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
In mathematics, you start with axioms - ground rules that must be true for anything else to be true. The axioms themselves have been proven. And it should be noted, that just about any axiom has a domain(s) for which is it valid and potentially many domains for which it is invalid.

So as a ground rule, we must take as a given that the Java compiler and runtime are trustworthy. Alas, sometimes they prove not to be, but we've got to start somewhere and to save time, we trust the testing that was done to ensure that our tools are reliable within the domain of our testing.

Likewise, we generally use a proven test framework and trust that it, too is reliable.

Finally, we try to keep our test code as simple as possible so that we can manually validation the test independently.

So mostly we're on top of a "pyramid of trust" here. We're not actually the only testers of the system, just the topmost layer.
 
Master Rancher
Posts: 4052
56
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
While I recognize this is in MD and intended as non-serious... this wouldn't be the first time someone took something in MD seriously.  As Fred of all people would know. ;).

So...

I think part of TDD is writing a test first, running it, and seeing it fail.  Then change the production code to make the test pass.  And see it succeed.  So you, as a human, are testing the test code, by observing the recurring alternation between failing and passing.  That's an important part of the process... if you don't see failures now and then, especially as you introduce new tests, it suggests either you aren't testing what you thought you were testing... or the tests aren't actually being run.
 
Mike Simmons
Master Rancher
Posts: 4052
56
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator

Tim Holloway wrote:The axioms themselves have been proven.



I think that sentence is missing a "not".
 
Tim Holloway
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator

Mike Simmons wrote:

Tim Holloway wrote:The axioms themselves have been proven.



I think that sentence is missing a "not".



Mike Simmons wrote:
I think part of TDD is writing a test first, running it, and seeing it fail.  Then change the production code to make the test pass.



No, no, no.

I have been solemnly assured by a co-worker that what you do in that case is update the documentation to say "Serious users do not consider this a problem". The idea being that users will be discouraged from whinging bout it lest they be considered clueless lightweights. Thereby saving both the effort of modifying tests (which we didn't have back then) and of actually fixing the production code.

Aside from that, the assertion was for test-driven development, not test-driven maintenance.

Now I, of course, never make misnakes and thus when I write my tests and then design application code to conform to the tests (which is how TDD works for me, anyway), then the tests of course are perfect and that's the end of it . They exist primarily to catch things like when someone has updated the specs such that blank spaces in CSV inputs require quoted fields or dates change from MM/DD/YY to YYYY-MM-DD. (that part is has actually happened to me, BTW).
 
Mike Simmons
Master Rancher
Posts: 4052
56
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator

Tim Holloway wrote:

Mike Simmons wrote:

Tim Holloway wrote:The axioms themselves have been proven.



I think that sentence is missing a "not".



The rest of your response seems to be tongue in cheek, but I'm thinking this part was more serious.  I may be mistaken.  Anyway, as I understand it, axioms are by definition unproven and unprovable.  They're the things that you stipulate as true without proof, because if you don't start with some basic ground rules, you can't prove anything else.  So you can't prove an axiom - if ever seems to be possible, then you've shown that the thing you've proven is not an axiom, and you may need to choose some other, better axiom to replace it.
 
Tim Holloway
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
I had to go back and check, since my definitions do tend to get sloppy when I don't. I'd say that an axiom is essentially self-proving, if you like

I should note that John von Neuman did mathematically prove that the architectures that we base computing on were valid, so there's where the turtles end.
 
Mike Simmons
Master Rancher
Posts: 4052
56
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator

Tim Holloway wrote:I had to go back and check, since my definitions do tend to get sloppy when I don't. I'd say that an axiom is essentially self-proving, if you like


I think "self-proving" is a myth.  People say that when they think something is obvious, but can't articulate why - at least, not in a logically rigorous manner that actually proves something.  Is there an example of an axiom that does prove itself, in a rigorous sense?
 
Tim Holloway
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
Well the Wikipedia's take on this is that:


Among the ancient Greek philosophers an axiom was a claim which could be seen to be self-evidently true without any need for proof.

I'm willing to take "self-evident" and "self-proving" to be tautologous as an axiom.

There is a branch of mathematics that does deal with self-proving theories, but that's getting a little outside our field, I think.
 
Mike Simmons
Master Rancher
Posts: 4052
56
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
I'm still comfortable with my previous statement - "people" in this case includes ancient Greeks. . I think they only say proof is not needed, because they found they had no way to prove their axioms.  Other than choosing a different set of axioms to start from.   But usually it was easier to just say "it's obvious" or "because I said so".  Some of those axioms of, say, Euclidean geometry, turned out not to necessarily be true in the real world.  Not Euclid's fault that he didn't know about curved spacetime and black holes.  So things can be self-evident and generally accepted as true... until they aren't.
 
Tim Holloway
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
Applying Euclidean axioms in non-Euclidean space is cheating.

There is such a thing as a Domain of Discourse.

 
fred rosenberger
lowercase baba
Posts: 13013
66
Chrome Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator

Mike Simmons wrote:As Fred of all people would know. ;).


I have no idea what you are talking about...
 
Mike Simmons
Master Rancher
Posts: 4052
56
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator

Tim Holloway wrote:Applying Euclidean axioms in non-Euclidean space is cheating.


But originally, they didn't know there was such a thing as non-Euclidean space.  They just thought those axioms were self-evident truths that didn't need to be proven.

And the real world itself isn't actually Euclidean, it turns out.  Even if there's some uncertainty as to the overall size and other details, phenomena like gravitational lensing have pretty well confirmed that space is curved, by gravity.  So those self-evident truths weren't actually true, in the real world.
 
Marshal
Posts: 74342
334
  • Likes 1
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
Ding! Ding! Ding!
End of round one!





















Ding! Ding! Ding!
Round two.
 
Campbell Ritchie
Marshal
Posts: 74342
334
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
They also were surprised to find out that numbers like √2 were irrational.

Didn't Douglas Adams once write that space‑time wasn't simply curved, but bent?
 
Tim Holloway
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
Again, it's cheating to apply one universe's set of rules to another universe. Unless you're playing Brockian Ultra-Cricket. Those guys have no shame.

Worse, it smacks of absolutism, where we assume that there is only One True Universe, and that's something that a lot of Einstein's heirs are still debating.

Within a Universe of Discourse, we can have Axioms and those Axioms are immutable, self-evident, and thus self-proving.

Consider this:


We hold these truths to be self-evident, that all men are created equal, that they are endowed by their Creator with certain unalienable Rights, that among these are Life, Liberty and the pursuit of Happiness.



Those are axioms upon which the USA was founded. And yet even at the time, this was manifestly not the case, as women, children and Negroes (including men) were all chattel and could be summarily deprived of the first two with little, if any control. Even today, the right to life depends very much on the size of your pocketbook, and sometimes liberty as well. We have a system that permits, if not encourages summary execution on the spot by police officers and your freedom includes the freedom to lose your life by starvation, disease or injury if you cannot obtain enough money to pay for them. An infant's "right to life" ends at birth.

So in short, axioms depend as much on what they leave out as what they include.
 
Mike Simmons
Master Rancher
Posts: 4052
56
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
So I'm with you on most of that... until you use the terms self-evident and self-proving.  Then things seem to go out the window, especially for the self-proving part which seems to mean something very different for you than for me.  I initially commented because I simply thought there had been a typo in your statement.  As that seems not to be the case, I'm finding diminishing interest in uncovering what "self-proving" means to you, or how that statement is useful to the conversation.  But, the rest seems to make sense, so maybe it's best to just leave it there.
 
Tim Holloway
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
Cogito, ergo sum.

Merriam-Webster wrote:
Proof
: the cogency of evidence that compels acceptance by the mind of a truth or a fact



Emphasis mine.
 
Mike Simmons
Master Rancher
Posts: 4052
56
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
Oookay.  That's not actually convincing me that self-evident and self-proving are the same thing.  Probably because I'm stuck on the part about compelling acceptance of a truth or fact. Are you only able to talk about axioms that you believe are true?  If I don't agree with  a particular axiom, is it therefore not an axiom, since it didn't compel acceptance and is therefore not self-proving or self-evident?  Personally I find it more useful to think of axioms as assumptions, which we may provisionally regard as true for purposes of a universe of discourse, while also allowing that there may be other universes of discourse with contradictory axioms.  
 
Tim Holloway
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
Axioms are the ground rules of any framework of discourse. The basis from which proofs derive. It would be pointless to accept a false rule, and as I said before, equally unacceptable to consider either axioms from other contexts or to accept said axioms automatically into other contexts. The axiom and its Universe of Discourse are inseparable. That doesn't mean that the same rule couldn't apply in other contexts, but it's the difference between equals() and "==", if you will.

Also, "agreeing" with an axiom strikes me as straight out of Orwell. Axioms don't care about whether you agree with them. They are the rules, and they are immutable. If the rules don't apply to all cases within their Universe then you didn't start with a complete set of rules. Newtonian physics became Einsteinian physics because we found out our rules were incomplete. And still are. Newtonian axioms are still valid within Newtonian math, but we have since widened our Universe of Discourse to include quantum and relativistic effects. But fortunately, digital computers are easier to map out.  It's a much smaller Universe.

I take Merriam-Webster as the basis of a syllogism:

1. Axioms are self-evident. Literally evidence of themselves.
2. Proof is compelled by evidence.

ergo,
3. Axioms are self-proving. Q.E.D.

In practical terms, that means that we have mathematical proofs for the basis of our computing model and thus, in theory can bootstrap up proofs all the way to the application tests themselves.

But that is very definitely with a specific domain in mind. If we used analog computers or devices whose outputs were statistical rather than determinate, then we'd have to have a different set of basic axioms.
 
Mike Simmons
Master Rancher
Posts: 4052
56
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
Regarding the "straight out of Orwell" comment, this mystifies me.  Belief is relevant here because you brought in a definition of proof that includes "compels acceptance".  That's why I referred to agreeing and disagreeing with an axiom in my response.  If you don't think it's proper to talk about belief in the context of axioms, why did you bring it up?  

I seem to be the one allowing for the possibility that not everyone may agree on an axiom, and yet it's still possible to talk about a universe where it's true, or another universe where a different set of axioms are true.  We can discuss Euclidean geometry, or various non-Euclidean geometries.  You on the other hand seem to imply that if something is declared an axiom, therefore it's proof of itself and compels others to believe its truth.  I, for one, am not compelled.  No, axioms don't care if you believe in them or not.  They're abstract concepts; they don't care about anything.  I, on the other hand, do care what I believe.  And I can talk about something that might be true, and the implications if it is true, independently of whether I agree with it.  I'm not sure where you have a problem with this.

Moving on...

Tim Holloway wrote:I take Merriam-Webster as the basis of a syllogism:

1. Axioms are self-evident. Literally evidence of themselves.
2. Proof is compelled by evidence.

ergo,
3. Axioms are self-proving. Q.E.D.


So the main issue we have seems to be around item 2.  Right now it's too ambiguous to form a real syllogism.

Here's a possible simplified version which is actually a rigorous syllogism:

1a. All evidence is proof.
2a. All axioms are evidence.
3a. Therefore, all axioms are proof.

I reversed the order of 1 and 2 to match the structure shown in Syllogism types.  Since the repeated middle term M is "evidence", 1a becomes the major premise, and 2a is the minor premise.

I realize I may well have changed something else  in a way you disagree with - but this is a reasonable approximation of how I understand your syllogism.  If you want to rephrase, feel free - hopefully it will help me better understand your thinking.  I know I dropped the "self" part for simplicity, for example, but I don't think that's pertinent to our disagreement.

If we accept 1a and 2a, they do indeed imply 3a.  It's a valid syllogism, modus Barbara.

I, however, do not accept 1a.  Nor is it implied by the Merriam Webster definition.  If the evidence is cogent enough that it compels acceptance by the mind, then it's proof, OK.  But if not, it isn't.  I think this is the root of our disagreement - at least from my side, it's when you seem to be implying something like 1a that I most strongly object.

Note that courtroom proceedings would be much simpler if we simply accepted that evidence is the same as proof.  But I, for one, am happy to live in a society that tries to recognize that these are not exactly the same thing.

It's perhaps tempting to convert this to a modified version:

1b. Some evidence is proof.
2a. All axioms are evidence.
3b. Therefore, some axioms are proof.

Except this is not a valid syllogism.  Some M are P, all S are M... doesn't imply anything further.  Because while all S are M, there may be other non-S that are also M, and when we are told that some M are P, we don't know if those M that are P come from the S or non-S population.  So we can't say that some S are P; we can't make that conclusion from these statements. That's why this would not be a valid form of a syllogism.

Perhaps there's another formulation that would be more agreeable to you?
 
Tim Holloway
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
I'll agree that the syllogism seems shaky, but I think that there's a tautologous situation in the second premise, and that should make it valid. Maybe someone can clarify that.

The "straight out of Orwell" means that just because The Party says that 2+2=5 doesn't actually make 2+2=5 no matter how many people want to believe that 2+2=5.

Bear in mind that we are working within a Universe of Discourse. Axioms are what define a Universe of Discourse. Don't mistake a  Universe of Discourse for some kind of "reality". The name means exactly what it says - a finitely-bounded playing field where the given axioms apply for the purpose argument. The rules of the game do not permit invalidating or fuzzing axioms. The only "belief" that applies are that you must "believe" that they are true. More to the point, you must know that they are true. Because if they are not true, you've got a leaky Universe.

As I said, the von Neumanm framework is what we are confining ourselves to. It is our Universe of Discourse and using the axioms that define that Universe, we can prove upwardly that an application is "correct".

But other computing systems do exist, some of them older than von Neumann's. And in the quantum realm, the main reason that 2+2 would not be equal to 5 would be that 2+2 could be simultaneously equal 1 and 7. Obviously different axioms apply there.

But that's someone else's problem.
 
fred rosenberger
lowercase baba
Posts: 13013
66
Chrome Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
My understanding of axions is that they are not, and have never been proven. However, they are supposed to be simple enough that you look at them and say "yeah...that makes sense.  That must be /is probably/is something i'm willing to accept as true". Then you use those to prove a bunch of other stuff.  As long as you don't end up with a contradiction, your system of mathematics is considered valid.

Euclid had five.  the first four were simple enough, but the fifth...it took more words to explain that the other four combined. He also seems to resist using it as long as possible...it shows up much later in his Elements than the other four.  But, the system we call Euclidian geometry is stable - no contradiction has been found.

Much later, someone noticed the fact that the fifth axiom was a little...sketchy (to use my daughter's terminology).  They were going to try and prove it by contradiction.  They assumed the opposite, and started working to develop a system of math based on that. They figured they'd get to some contradiction, which would invalidate their assumption.  They never found one.  The only conclusion is that both systems are valid, in the right circumstances.  And neither system is valid without assuming some version of the fifth is true.

The Gödel came along and screwed everyone over - but that's a whole other topic i'd need to brush up on.

 
Tim Holloway
Saloon Keeper
Posts: 24499
167
Android Eclipse IDE Tomcat Server Redhat Java Linux
  • Mark post as helpful
  • send pies
    Number of slices to send:
    Optional 'thank-you' note:
  • Quote
  • Report post to moderator
I think the heart of the argument is that while I'm referencing the concept of a limited Universe, others are thinking of an Absolute ("real") Universe.

It's like the old joke: "Define Universe and give 3 examples".

In recent years, cosmologists have considered the concept of a Multiverse - a larger space containing multiple universes, each of which might contain different characteristics. Everything from "going down the other leg of the Trousers of Time" to Universes where fundamental constants like the speed of light are not the same.

But physical Universes aside, Mathematics has its own concepts that may be inspired by real-world observations but then have taken flight in their own directions. This gives us such things as the Calculus of Propositions, an essential underpinning of modern digital computing and Number Theory. I have actually run into projects where certain key concepts of a project were handed over the the local University Math Department for rigorous proofing.

You can have all sorts of Universes - integer numbers, boolean expressions, even states in a Version Control System like Git.

At their heart, they all have basic principles, and a synonym here for "basic principle" is axiom. The singular characteristic of an axiom is that since it defines the Universe in question, there's no point in questioning it. If the axiom is not true, then neither is the Universe.

In physics, we have learned that the original Axioms used for the physical Universe are not complete. In digital computation, we're pretty sure that the axioms are complete. If a JVM fails to perform a test properly, we look for a bug in the JVM - we don't assume that the axioms of computation are at fault.

There is probably a mathematical term for a condition where the axioms are not complete and even for Universes where axioms cannot be complete. But I think we have enough problems already.
 
reply
    Bookmark Topic Watch Topic
  • New Topic