Programming and Electronics

Name | |
---|---|

Subject | |

Comment | |

File | |

Embed | |

Password |

Hop in to our IRC channel! #wirechan@rizon.net

File: 1599760604718.jpg (1.09 MB, 1200x1600, ba78fa26952a7c71999c7cfa23….jpg)

If Curry–Howard correspondence is true and proofs are programs, why don't software engineers just write proofs instead of programs? That we they wouldn't have to worry about proving their programs correct since they would be already proofs.

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.

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

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:

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.

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.

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

- Tinyboard + vichan 5.1.4 -

Tinyboard Copyright © 2010-2014 Tinyboard Development Group

vichan Copyright © 2012-2016 vichan-devel

All trademarks, copyrights, comments, and images on this page are owned by and are the responsibility of their respective parties.

We are an independantly owned chan, not related or co-owned in conjuction with any other chans.

All posts on Wirechan are the responsibility of the individual poster and not the administration of Wirechan.

re:wire group © 2017-2020