What do you call a statement P which has never been formally proved but all the observations so far verify it? This question comes from this scenario: some people use a software for work. They often use a specific function. When this function was designed, the developers feared that some errors might occur. However, these errors never occur and workers have used it for years. Of course this function works correctly, because it has never failed. However, no developer has ever taken the time to understand how. In this example, P is the statement "this function is error free".
It's not clear what you're asking now, after your edit. The statement "this has always worked even though we don't know how" is simply true (taking your word for it). So to which statement are you referring when you say "statement that has never been proven"? Do you mean to ask: how do we call a situation in which we don't know how something works?
Commented Apr 29, 2016 at 16:49@EliranH Alberto is describing an induction. "We don't know for sure that the software will continue to work, because we can't prove that it will, but it has always worked in the past so we think it will keep working." The unproven claim is it will keep working.
Commented Apr 29, 2016 at 17:05What does "this functionality" mean? Don't you mean "this program"? Proof is about propositions/programs, not functionality.
Commented Apr 29, 2016 at 20:02It partly depends on the subject area that the statement falls into, and how it has been supported by facts (e.g. merely not yet contradicted vs. rigorously tested and corroborated). Building off the comments:
You might call this a conjecture if it relates to math or logic, or if it has not been well-corroborated yet.
In science it would be called a hypothesis.
A more general term would be an [epistemic] possibility. Note that it's epistemic because we're talking about evidence and ways we might know something is true; modality isn't really relevant.
Edited after the question:
Your example is interesting because it doesn't seem to fit perfectly into the terms that have been suggested. I would argue that this is a more general case of an inductive claim ("It's always worked in the past, therefore it will continue to work"). You could call the conclusion that it will continue to work an induction. This follows the pattern of referring to a deduced conclusion as a deduction.
Socrates is wise, and Socrates is a man. My deduction is that some men are wise.
Every time I have dropped an apple near the surface of the earth, it has fallen downward. My induction is that it will continue to do so in the future.
This is a slightly unusual usage, I admit, but I think it fits your situation the best.
answered Apr 29, 2016 at 15:39 836 7 7 silver badges 12 12 bronze badges Thanks for the answer. See my edits if you need clarifications. Commented Apr 29, 2016 at 16:37 @Alberto I've edited my answer with another suggestion. Commented Apr 29, 2016 at 17:03Thank you @Era, the apple example is exactly what I was trying to say. I think the induction fit my case.
Commented Apr 29, 2016 at 19:06 Thank you @Era, I found that "conjecture" was the correct word Commented Jan 19, 2017 at 15:05Since your question pertained to software, here is a software-related answer: Software that is used in production for years and has not yet failed is called either reliable or mature.
This does not make any assumption about its actual correctness. Both terms only say that it has worked so far under real world usage, not that it has been proven to be correct under any circumstance.
Of course this funcionality is correct, because it has never failed
This is an invalid conclusion. Just because it has not yet failed does not mean it won't in the future. We can't be sure.
There are ways to prove that certain porperties hold under certain conditions, and that is done rigoruously in critical software. Some pieces of software, like the VxWorks OS, are expected to have only one BSOD every 30 years.
answered Apr 29, 2016 at 21:57 119 6 6 bronze badgesFor the specific software situation you're describing, take a look at Hoare Logic, as discussed, e.g., in https://en.wikipedia.org/wiki/Hoare_logic
In this model, your program's correctness is determined by a collection of Hoare Triples of the form C , where =preconditions/input, C=your_program, =postconditions/output. Given input satisfying any of the prescribed preconditions, if your program's output satisfies the corresponding postconditions, then it's "correct".
As a simple example, suppose C=program_to_add_two_numbers. Then one Hoare Triple might be C , where =both_numbers_to_be_added_are_odd, and =sum_is_even. Obviously, that one Hoare Triple by itself doesn't establish C's correctness. But an appropriate collection of Hoare Triples usually does. ("Usually" means whenever there exists a collection of Hoare Triples that uniquely, in an if-and-only-if sense, specifies the function : input-->output to be calculated.)
And you might want to check out some of the "See Also" links at the bottom of that wikipedia article for several other models of program correctness. As you might imagine, computer science has devoted lots of rigorous investigation to this subject.
edit: Thanks, @JamesKingsbery Regarding your "term for this concept" remark, yes, I should have explicitly mentioned that you can google the term "program correctness" for lots of additional information.
answered May 2, 2016 at 11:43 user19423 user19423Welcome to Philosophy.SE! Great answer to the question, I didn't know there was a term for this concept!
Commented May 2, 2016 at 14:51As I understand standard usage, a formally provable sentence is a theorem, so "P is a theorem" says that P is true and that the claim that P is true is justifiable by deductive proof. A conjecture is proposed as true, but without formal justification, either deductive or inductive. Empirical claims are never formally provable, so their justifications are either inductive or abductive. This is true even for "laws"; e.g. Ohm's Law is not the sort of thing that can be formally proven. The best we can do is conduct lots of experiments, observe that it never fails to hold, and infer (inductively? abductively?) that is must be true. Then we call it a theory (about the natural world).
I think your use case is fundamentally different. We don't normally call programs theorems, tho we could if we prove them correct. More likely we would call them "certified" or the like. A program that is not formally proven to be correct, but that has never failed, is not really like a an empirical theory, because is is not a natural artifact. Such a program could in principle be proven correct or incorrect, unlike an empirical claim.
I would suggest drawing on engineering rather than logic, and call such programs reliable. This has the advantage of removing the notion of truth, which is a philosophical issue of no relevance to engineering. It also has a nice formal statistical definition that I won't bore you with, and it's related to notions like robustness, since the justification for reliability claims will involve variance: if your code has been running for 10 years without error, but always with the same input, then it may be reliable for that input but you have no idea how robust it is, i.e.whether it is reliable under different conditions.