3 ms·
> 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
by gravypod 10y ago
> 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.
- pka 10y ago> 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.
- gravypod 10y agoOk so if you are given a specification and you use formal methods throughout and it doesn't conform to the specification you were provided with at the end you have made an error. The specification is not at fault here. What you are doing is claiming types into and out of functions decide if they are functioning correctly. This is not the case at all. I think that most bugs aren't because the type you were expecting was wrong but the data produced by a function was wrong. Implementations cannot be judged just because they accept the correct types. For instance, if I am told to write a function to predict lottery numbers and do the following LoteryNumberType get_lottery_number :: LotteryNumberType If I call `get_lottery_number` by your logic it will always provide me with the real winning lottery number since the types check out. That is absolutely incorrect. Types can't prove functionality. They do provide protection from a set of bugs but those bugs are also avoided easily by handling every case that a function can return which was already being done before formal methods where an idea. You can't say a program will have no bugs because the types check out. Is that what you are saying? Your code's types match in all uses -> this means there are no bugs -> this means I don't need to test my code? Is that really what you think?