Proving code

Stream: general

[Alice Laroche]

Hi,

I wanted to write and prove some code, but passing down proof needed for all function to work well is tedious
Is there a better patern than that ?

[Yaël Dillies]

Use junk values!

[Arthur Paulino]

@Alice Laroche it depends a lot on your use case and design. Can you be more specific on what you want to do? Maybe pointing out some code that you already have in place

[Alice Laroche]

For exemple let's say i want to use nth or nth_le
If I use the first i need to propagate option something all the way up only for proving it will never be none so using option to begin with seem unnecessary
If i use the second i need to pass proof from function to function to pass the proof needed by nth_le , but it create a mess because all my functions become dependant type
So i was wondering if there was a third option

[Yaël Dillies]

Instead of using option, you can return a junk value. For example docs#real.sqrt returns 0 on negative reals.

[Alice Laroche]

In many case junk value don't exist because they could mean something else

[Arthur Paulino]

Is it possible to match and resolve the option something right before the first function call so you don't have to pass option something through your pipeline of functions?

[Alice Laroche]

I don't think so, like i said it's very like nth Is there a third way of writing nth that don't use neither option or a proof of absurdity

[Yaël Dillies]

Maybe you want to bind the options? Monadic programming? I'm just guessing at this point. A MWE would be very helpful.

[Yaël Dillies]

Alice Laroche said:

I don't think so, like i said it's very like nth Is there a third way of writing nth that don't use neither option or a proof of absurdity

Yes, making it return a junk value.

[Yaël Dillies]

That's how docs#list.head works, for example.

[Alice Laroche]

Errh, i think i wanted something like throwing an exception and prove that never happen, but now i feel stupid about that
option is the best choice

[Mario Carneiro]

There is a function docs#option.get that will allow you to extract the value from an option if you prove it is non-none. So this is roughly equivalent to "throw an exception and prove that it will never happen"

[Mario Carneiro]

Alternatively, you can use a precondition which is crafted specifically to discharge any side conditions that arise; then you have to prove at the top level that the precondition can be satisfied. This is essentially the dual approach; with both methods writing the program is easy and proving that it is total is hard