/g/ - Technology

I'm glad u asked.

>why don't software engineers just write proofs instead of programs
Well, technically, they do write proofs, since programs are the same thing.
The things is, they usually prove something like:
"given integers x,y, either floor(x/y) is an integer or RuntimeException".

I guess are asking why their proofs almost always prove this extra " or RuntimeException" (and actually there are usually more such terms).
The reason is just that it's easier to not be as precise, at least with the current technology.
For example, if i can use (int)( x*(x+2)/2 ) without having to prove that x*(x+2)/2 is an integer.

There are some languages whose programs really are proofs (e.g. Coq),
but they are more difficult to read and write, have less access to libraries, etc.

I think there should be a way to write safe, yet readable and efficient code,
but i haven't seen any way how.
Maybe some people can help me there.

>>389
That's not entirely correct. What you describe is the typechecking, which is equivalent to the correctness check of a proof. But the statement that the proof proves is not this, but the type itself. If your proof is "floor(x/y)", what it proves is that if you can construct two integers, then you can construct an "integer or RuntimeException".

It's easier if we put it in a method. The following three methods have the same type and therefore prove the same statement:

int nonsense(int x, int y) throws RuntimeException {
    return floor(x/y);
}
int nonsense2(int x, int y) throws RuntimeException {
    return 0;
}
int nonsense3(int x, int y) throws RuntimeException {
    throw new RuntimeException();
}

Here's a more interesting example. Let's say we have a class "foo", that has no constructors and cannot be constructed in any way. Despite this, if we were to use Java's type system to prove things, the following would be proof that we can construct foo (given that we can construct an int), which is obviously not correct:

foo bullshit(int x) {
    return bullshit(x);
}

In a proof assistant "foo" could stand for a type claiming "P = NP" or even "1 = 2". For this reason, in Coq you have to prove that every program that you wrote terminates. In most cases Coq does it automatically for you, but in the other cases it can get very complicated.

>>390

>That's not entirely correct.
What i should've said is that, in hypothetical a program,
the expression floor(x/y) proves that, given integers x,y, either you can make an integer or throw a RuntimeException.

>throws RuntimeException
In every Java declaration,
there is an implicit RuntimeException,
since they can be thrown anywhere without declaration,
so any method's return type should be considered a union of the stated type with a RunTimeException throw.

> return bullshit(x);
I guess we should add an "infinite execution" to all our RuntimeException terms.
You could also return null,
the fact of which i would interpret as all object types actually being union types with null.

>which is obviously not correct
Ya, adding any of the aforementioned terms
causes the significance of types to deviate from what one would expect
and makes the type system trivial,
but it then it does correctly describe how Java works.

>in Coq you have to prove that every program that you wrote terminates
As a consequence, Coq is not Turing complete.
This doesn't really restrict you in any profound way though,
since algorithms are usually designed to terminate with some useful result anyways.