Well, an F to C converter is not a terribly interesting case, because it would be trivial to implement. When you think about it, how would you test this in your favourite language of choice? By computing the expected value by using the same formula you used to compute the value you are testing in the first place.

But here's another example that came up recently. Let's say you want to write a function that takes a string and returns its first character. Now, it would be an error to call this function with an empty string, because then what would it return?

In a normal language, you'd probably check if the string was empty and then return null or something. When testing the function, you'd have to remember the empty string case and write an unit test for it (now I don't know about you, but I can't say I'd always remember to write a test case for this particular edge case; normally I'd forget).

Can we do better? It turns out we can.

We can encode invariants about our program on the type level. Types can be more than just strings, ints and chars. They can also be propositions, i.e. statements about our program. In this particular case we can construct a type

    NonEmptyString

that can only be constructed by a function like this (using Haskell syntax):

    neString :: String -> Maybe NonEmptyString

(This means that neString takes a String and returns a Maybe NonEmptyString). But what is this Maybe (also called Option, etc)?

It's like a union type - it can either contain some value, or it must be empty. Now the cool thing about Maybe is that we can't just take out the potential value contained inside it - we have to pattern match on it! What this means is, that whenever you want to see what's inside a Maybe the compiler forces you to tell it what to do in both cases - when there's something inside and when there's nothing inside.

Maybe you can see where this is going. This is how our takeFirstChar function would look like:

    takeFirstChar :: NonEmptyString -> Char

Notice - we say that it only works on NonEmptyStrings! If we try to pass a regular string to it that would be a compiler error. But now we want to read something from the command line and returns it's first char. Let's say we have a read function:

    read :: String

Every time you call this function it gives you a string read from the terminal. Ok, let's put our program together now:

    a = read
    print (takeFirstChar a)

But wait! We can't do that - as I said above, the compiler complains, because we try to pass a String to a function that expects a NonEmptyString. Instead we have to:

    a = read
    case (neString a)
      Just st: print (takeFirstChar st)
      Nothing: print "String was empty"

Notice how we pattern match on the result of (neString a). If the string was empty, we'd match the Nothing clause. In all other cases we'd print the first char.

What we did is prove that the program will behave correctly in all cases - no tests needed! We can't put the program together in any other way, because it would be a type error. In a sense, the fact that the program exists is a proof of its type (programs have types too!)

Now this is a pretty trivial invariant to encode on the type level, but in a dependently typed language you could encode whatever you'd like, i.e. for example that a list is sorted or that a number is the GCD of two other numbers, etc.

This is often not trivial to do, and at some point you start seeing diminishing returns, because the time it takes to rigorously encode a proof is longer than any possible return of investment caused by proving that there are no bugs. But doesn't have to be an either-or situation. You can encode as much invariants as you'd want in your code. I think Haskell strikes a good balance in that regard, although Idris is a very interesting language too.

(Sorry for typos, errors etc, didn't proofread).