Types, programs and proof.

Stream: Program verification

[Jason Foutz]

I mean this in the kindest, gentlest way possible. Dependent types are new.

it would be really nice if there was some syntax to say, X is the type I'm targeting. Y is the process I believe will satisfy that type, and finally Z is the proof Y satisfies X. I'm super new, and probably in the wrong channel. and I'm happy to move somewhere else.

I understand and have deep sympathy for encoding 3 different things in a linear text file. Perhaps I'm just venting.

Sigma offers pairs, and I'm free to choose, do I want to encode the proof Or the type or the proof? I don't know. I'm new. Do you bundle up arguments and proofs, or do you put the arguments up front, and then the proofs trailing at the end? I don't know. I'm new and dumb.

But I feel like there is space for <type, process, proof>. Perhaps I'm missing something fundamental. But I feel like these 3 together sort of make the language. No complaints. I'm getting there. sigma helps, but pairs don't really capture the space. Perhaps I just need to be smarter.

<type, process, proof> seems to capture all of the difficulties I've encountered. might make it easier for other folks.

[Chase Norman]

Types in dependent type theory are specifications. If you produce a program of a particular type, it necessarily has the specification. So, Y : X is all that is needed in principle. If there are additional properties of Y that X does not reflect, then additional types may be constructed that involve explicit reference to Y.

For instance, constructing a program f of type (n : Nat) -> Fin (n + 1) already suffices to guarantee that the output is less than or equal to the input. However, if you also want to show that the output is always even, you can show (n : Nat) -> Even (f n).val. In reality, this second type is just another program, that happens to return a proposition instead of data.