2 ms·

Ok 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 h

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

pka 10y ago
> 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. When I say proof, I mean it in the mathematical sense. The Curry–Howard isomorphism [0] formalizes the relationship between (mathematical) logic and type theory. Unless you are saying mathematical logic is inconsistent (and thus every mathematical proof is invalid) this is absolutely the case. The same way you can construct a mathematical proof that e.g. n is prime, you can can construct a type Prime n that proves that n is prime [1]. > I think that most bugs aren't because the type you were expecting was wrong but the data produced by a function was wrong. This is where your misunderstanding stems from. Continuing with the example from above, if you have a function: makePrime :: n -> Prime n the function can not construct (Prime n) if n is not a prime. > 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. If you give me a specification that constructs predicted lottery numbers I could absolutely turn it into a type :) > They do provide protection from a set of bugs but those bugs are also avoided easily by handling every case But you don't have proof that you are handling every case :) > You can't say a program will have no bugs because the types check out. Is that what you are saying? Yes, if the types correspond to the specification then there are no bugs. The specification can still have bugs though, but that's unavoidable. The thing is that you've proven the program does what you told it to do. Once you stop thinking about types in the Java sense and start thinking about them as logical propositions it will all make sense. I provided you with a couple of links in the other comments and here if you are still interested. [0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [1] https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Primality.agda https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat...

pka 10y ago

> 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. When I say proof, I mean it in the mathematical sense. The Curry–Howard isomorphism [0] formalizes the relationship between (mathematical) logic and type theory. Unless you are saying mathematical logic is inconsistent (and thus every mathematical proof is invalid) this is absolutely the case. The same way you can construct a mathematical proof that e.g. n is prime, you can can construct a type Prime n that proves that n is prime [1]. > I think that most bugs aren't because the type you were expecting was wrong but the data produced by a function was wrong. This is where your misunderstanding stems from. Continuing with the example from above, if you have a function: makePrime :: n -> Prime n the function can not construct (Prime n) if n is not a prime. > 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. If you give me a specification that constructs predicted lottery numbers I could absolutely turn it into a type :) > They do provide protection from a set of bugs but those bugs are also avoided easily by handling every case But you don't have proof that you are handling every case :) > You can't say a program will have no bugs because the types check out. Is that what you are saying? Yes, if the types correspond to the specification then there are no bugs. The specification can still have bugs though, but that's unavoidable. The thing is that you've proven the program does what you told it to do. Once you stop thinking about types in the Java sense and start thinking about them as logical propositions it will all make sense. I provided you with a couple of links in the other comments and here if you are still interested. [0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [1] https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Primality.agda https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat...