> 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?

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.

From there, if given null you should return null back or throw an exception depending on the language.

My function would, abstractly, look:

  function get_first_letter(s):
    if s == null:
      return null
    if s == "":
      return ""
    return s[0]
  
  value = get_first_letter(read_string())
  
  switch (value):
    case null:
      print("No string entered")
      return
    default:
      print(value)
      return

Is this code "proven" just because it handles a every case? What makes this a proof or proven? This is basically just good practice: handle every case that a function can create. This is something that we have all been doing. Why makes a formal method "proven" or different.

> 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!)

This seems no different from any other language. You've just spread the code you had to write over "neString" and "takeFirstCharacter" and created a new type for it. Why couldn't you have just used the underlying functionality of String to make those checks when needed? For instance, "neString" must be using some sort of string method to check if a String is a NotEmptyString. Why not just put that code where it needs to be?

This just seems like a way to force your hand into using More types that have the same underlying implementation and I just see that as a way to confuse someone trying to come work on your project. When I look at source and say "wait a minute they have 10 types defined for strings and all they do is something that String could do beforehand" I'm a little irked. What makes the implementation that you have created "proven"? Just that the compiler said that all of the types line up? That doesn't make you any safer then before.

If you even make a single cast, a single unsafe block, or anything then you need to test the entire system. Your house of type-verifying cards falls down once you hit even the smallest section of unverifiable code. Just by making types for every one of your billion special cases doesn't mean that you don't need to test the code.

For instance in rust the standard library uses unsafe{} blocks often. This means that any code that goes into or comes out of that block is unverifiable for type. Just by using defined types to create it doesn't make it so the programmer has correctly implemented anything.

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.

You can't just make more types and call it all good.