What do you call a statement that is accepted as true but has never been proved?

Question

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".

Answer 1

It 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.

Answer 2

Since 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.

Answer 3

For 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 {P}C{Q}, where {P}=preconditions/input, C=your_program, {Q}=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 {P}C{Q}, where {P}=both_numbers_to_be_added_are_odd, and {Q}=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.

Answer 4

As 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.

Answer 5

They are called, statements accepted "on faith," "on trust," or "with reservations." An example of this, is the statement - good people go to heaven. The credibility of this statement depends more on the credibility of (trust on) the person making it, than on the statement itself.

With respect to software programs/functions in particular, this is an entirely different thing. A program is made by a person(s), so whether a program will "always" work, under "all possible" conditions, is a function of how thoroughly the programmer covered all such error possibilities and how thoroughly the test department did their job. Obviously, the more thorough these activities were done, the less likely the program will fail. However, the high probability of "human errors" makes it impossible to guarantee that any particular program (or function) will always work under all conditions! Therefore, the statement "this function is error free," needs to be preceded by "so far, this...", to make it a "sensible" statement (a statement that makes sense).

Answer 6

A statement that is accepted as true but has never been proven? In mathematics you would call it "incorrectly accepted as true".

Even in software development, where standards will be lower, nobody in their right mind would ever call any software "error-free". You may hear that software has "no known bugs" or "no reported defects".