[vertex-four]

OK, let's put it this way. I have an entirely arbitrary calculation, taking input A and outputting B. I want to ensure that this calculation is implemented according to specification.

How on earth do you write a type, or set of types, for that that actually bear some resemblance to the spec and don't simply reflect the details of the implementation?

To simplify it to the point of near-nonsense, how would you write a type which says `append "foo" "bar"` will always result in "foobar", and never "barfoo" or "fboaor"? Or that a theoretical celsiusToFahrenheit always works correctly and implements the correct calculation? If you can't do that, how can you do it for more complex data transforms?

[chongli]

This is where dependent types come in. They allow you to write an implementation of append that is correct by construction. Your algorithm is in essence a formal proof of the proposition that `append foo bar = foobar`.

A simpler example is that of lists and the head operation. In most languages, if you try to take the head of an empty list you get a runtime exception. In a language with dependent types you are able to express the length of the list in its type and thus it becomes a type error (caught at compile time) to take the head of an empty list.

[vertex-four]

> Your algorithm is in essence a formal proof of the proposition that `append foo bar = foobar`.

Isn't that literally just implementing the program, though? The point of tests is that they're simple enough that you can't really fuck up, and they describe the specification, not the implementation.

If you have to write a formal proof, what's making sure the proof is actually proving what you intend? And what's the actual difference between this proof and the implementation?

[chongli]

If you have to write a formal proof, what's making sure the proof is actually proving what you intend? And what's the actual difference between this proof and the implementation?

The formal proof is the implementation. It is the code you run in production. The proposition is your types. Instead of writing tests, you write types. It's the exact same process you would use with "red-green-refactor" TDD except it's the compiler checking your implementation instead of the test suite. The advantage of doing it with types is that the compiler can actually infer significant parts of the implementation for you! Types also happen to be a lot more water-tight than tests due to the way you specify a type for a top-level function and everything inside of the body can generally be inferred.

If you're interested, here is a series of lectures demoing dependently-typed programming in Agda by Conor McBride:

https://www.youtube.com/playlist?list=PL_shDsyy0xhKhsBUaVXTJ...

[vertex-four]

I will certainly watch those - but for the moment, I see no obvious way to immediately see that a proof is proving what you intended it to prove, whereas `assert (append "foo" "bar") == "foobar"` immediately shows what you expect and can be read and checked by somebody with the slightest programming knowledge.

The point of tests is that they're supposed to be simple enough that it should be near-impossible for them to contain bugs - they're incomplete, sure, but what they're testing should always be correct - whereas it seems that it would be easy for a proof to prove something subtly different from the spec without anybody being able to tell. If we could write complex programs to spec without error, we wouldn't have tests in the first place.

[chongli]

You don't have to see that the proof is proving what you intend; the type-checker does that for you. This is why some people sometimes refer to type checkers as small theorem provers.

As for your assert example, how do you know append will work as you expect for all possible strings (including null characters or weird unicode edge cases)? With a proof you will know.

[vertex-four]

> With a proof you will know.

But I could just as easily accidentally write a proof which proves something else, couldn't I? This is complex code expressing complex ideas - a type system would certainly help, but it can't tell me that I'm proving the wrong thing.