> This is wrong because it depends on the language. The behavior depends on the implementation but if you are meant to return the first character in the string and the string has no characters then you should return an empty string if provided a string with no characters.

How? The type is:

    takeFirstChar :: String -> Char

There's no such thing as an empty char. Your get_first_letter essentially has the type:

    get_first_letter :: Either Null String -> Either Null String

Which doesn't guarantee anything and is arguably a lot worse than just:

    get_first_letter :: NonEmptyString -> Char

This is why you can't have proven code in a lot of languages, because they permit you to lie about the actual types. From there, any proof is invalid because it is based on invalid propositions.

Dependently typed and other languages do not allow you to lie about the types (for example, a value can't be null unless this is reflected in the type; you can't throw exceptions or do IO unless this is reflected in the type, etc), hence a well typed program in such a language is a valid proof. You can not implicitly cast between types, i.e. a function like:

    cast :: a -> b

doesn't exist.

A function like print actually has the type:

    print :: String -> IO ()

Which tells you that it is doing IO. You can't call such a function from a pure function for example, the types wouldn't permit it.

> Also, you are assuming the implementation of neString is correct. What if that has a bug? Again, just because your passing your data around the correct way doesn't mean the correct things are happening with it.

I was simplifying, but neString would actually have a type similar to:

    neString :: String n -> Maybe (String (n != 0))

where n is the length of the string. Notice, the length is encoded in the type! A wrong implementation (one that returns i.e. Maybe (String 0)) will not type check.

But yes, you can have errors in your proof, no doubt. But these are specification errors, which there's no way to get around. What a proof guarantees is that there are no errors in the implementation of your specification.