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