How many lines of code is Candy Japan?

Re:How many lines of code is Candy Japan? by exi2 on Friday September 30, 2016 @12:28PM (#12613461)

I highly doubt that you can prove correctness with types alone.

How would you verify the correctness of this function with types alone:

Integer add(Integer a, Integer b) { return a + b; }

How would types verify for me that the result is correct and not a+b+1?

Formal proofs work for this but to make them work you need more than just types.

[ Parent | on HN ]

Re:How many lines of code is Candy Japan? by omaranto on Friday September 30, 2016 @02:27PM (#12614268)

The return type of your function is too broad: It should be the "type of integers which can be proven to be the sum of a and b".

That sounds like a joke but it's what going overboard with dependently typed programming languages is like.

[ Parent | on HN ]