2 I accidentally a verb
source | link
  1. It is a lot easier to reason about code when everything is immutable. As a result, loops are more often written as recursion. In general, it's easier to verify correctness of a recursive solution. Often, such a solution will also read very similarly to a mathematical definition of the problem.

    However, there is very little motivation to carry out an actual formal proof of correctness in most cases. Proofs are difficult, take a lot (human) time, and have a low ROI.

  2. Some functional languages (esp. from the ML family) have extremely expressive type systems that can make much more complete guarantees that a C-style type system (but some ideas like generics have become common in mainstream languages as well). When a program passes a type check, this is a kind of automated proof. In some cases, this will be able to detect some errors (e.g. forgetting the base case in a recursion, or forgetting to handle certain cases in a pattern match).

    On the other hand, these type systems have to be kept very limited in order to keep them decidable. So in a sense, we gain static guarantees by giving up flexibility – and these restrictions are a reason why complicated academic papers along the lines of “A monadic solution to a solved problem, in Haskell exist.

    I enjoy both very liberal languages, and very restricted languages, and both have their respective difficulties. But it's not the case that one would be “better”, each is just more convenient for a different kind of task.

Then it has to be pointed out that proofs and unit testing are not interchangeable. They both allow us to put bounds on the correctness of the program:

  • Testing puts an upper bound on correctness: If a test fails, the program is incorrect, if no tests fail, we are certain that the program will handle the tested cases, but there may still be undiscovered bugs.

    int factorial(int n) {
      if (n <= 1) return 1;
      if (n == 2) return 2;
      if (n == 3) return 6;
      return -1;
    }
    
    assert(factorial(0) == 1);
    assert(factorial(1) == 1);
    assert(factorial(3) == 6);
    // oops, we forgot to test that it handles n > 3…
    
  • Proofs put a lower bound on correctness: It may be impossible to prove certain properties. For example, it may be easy to prove that a function always returns a number (that's what type systems do). But it may be impossible to prove that the number will always be < 10.

    int factorial(int n) {
      return n;  // FIXME this is just a placeholder to make it compile
    }
    
    // type system says this will be OK…
    
  1. It is a lot easier to reason about code when everything is immutable. As a result, loops are more often written as recursion. In general, it's easier to verify correctness of a recursive solution. Often, such a solution will also read very similarly to a mathematical definition of the problem.

    However, there is very little motivation to carry out an actual formal proof of correctness in most cases. Proofs are difficult, take a lot (human) time, and have a low ROI.

  2. Some functional languages (esp. from the ML family) have extremely expressive type systems that can make much more complete guarantees that a C-style type system (but some ideas like generics have become common in mainstream languages as well). When a program passes a type check, this is a kind of automated proof. In some cases, this will be able to detect some errors (e.g. forgetting the base case in a recursion, or forgetting to handle certain cases in a pattern match).

    On the other hand, these type systems have to be kept very limited in order to keep them decidable. So in a sense, we gain static guarantees by giving up flexibility – and these restrictions are a reason why complicated academic papers along the lines of “A monadic solution to a solved problem, in Haskell”.

    I enjoy both very liberal languages, and very restricted languages, and both have their respective difficulties. But it's not the case that one would be “better”, each is just more convenient for a different kind of task.

Then it has to be pointed out that proofs and unit testing are not interchangeable. They both allow us to put bounds on the correctness of the program:

  • Testing puts an upper bound on correctness: If a test fails, the program is incorrect, if no tests fail, we are certain that the program will handle the tested cases, but there may still be undiscovered bugs.

    int factorial(int n) {
      if (n <= 1) return 1;
      if (n == 2) return 2;
      if (n == 3) return 6;
      return -1;
    }
    
    assert(factorial(0) == 1);
    assert(factorial(1) == 1);
    assert(factorial(3) == 6);
    // oops, we forgot to test that it handles n > 3…
    
  • Proofs put a lower bound on correctness: It may be impossible to prove certain properties. For example, it may be easy to prove that a function always returns a number (that's what type systems do). But it may be impossible to prove that the number will always be < 10.

    int factorial(int n) {
      return n;  // FIXME this is just a placeholder to make it compile
    }
    
    // type system says this will be OK…
    
  1. It is a lot easier to reason about code when everything is immutable. As a result, loops are more often written as recursion. In general, it's easier to verify correctness of a recursive solution. Often, such a solution will also read very similarly to a mathematical definition of the problem.

    However, there is very little motivation to carry out an actual formal proof of correctness in most cases. Proofs are difficult, take a lot (human) time, and have a low ROI.

  2. Some functional languages (esp. from the ML family) have extremely expressive type systems that can make much more complete guarantees that a C-style type system (but some ideas like generics have become common in mainstream languages as well). When a program passes a type check, this is a kind of automated proof. In some cases, this will be able to detect some errors (e.g. forgetting the base case in a recursion, or forgetting to handle certain cases in a pattern match).

    On the other hand, these type systems have to be kept very limited in order to keep them decidable. So in a sense, we gain static guarantees by giving up flexibility – and these restrictions are a reason why complicated academic papers along the lines of “A monadic solution to a solved problem, in Haskell exist.

    I enjoy both very liberal languages, and very restricted languages, and both have their respective difficulties. But it's not the case that one would be “better”, each is just more convenient for a different kind of task.

Then it has to be pointed out that proofs and unit testing are not interchangeable. They both allow us to put bounds on the correctness of the program:

  • Testing puts an upper bound on correctness: If a test fails, the program is incorrect, if no tests fail, we are certain that the program will handle the tested cases, but there may still be undiscovered bugs.

    int factorial(int n) {
      if (n <= 1) return 1;
      if (n == 2) return 2;
      if (n == 3) return 6;
      return -1;
    }
    
    assert(factorial(0) == 1);
    assert(factorial(1) == 1);
    assert(factorial(3) == 6);
    // oops, we forgot to test that it handles n > 3…
    
  • Proofs put a lower bound on correctness: It may be impossible to prove certain properties. For example, it may be easy to prove that a function always returns a number (that's what type systems do). But it may be impossible to prove that the number will always be < 10.

    int factorial(int n) {
      return n;  // FIXME this is just a placeholder to make it compile
    }
    
    // type system says this will be OK…
    
1
source | link

  1. It is a lot easier to reason about code when everything is immutable. As a result, loops are more often written as recursion. In general, it's easier to verify correctness of a recursive solution. Often, such a solution will also read very similarly to a mathematical definition of the problem.

    However, there is very little motivation to carry out an actual formal proof of correctness in most cases. Proofs are difficult, take a lot (human) time, and have a low ROI.

  2. Some functional languages (esp. from the ML family) have extremely expressive type systems that can make much more complete guarantees that a C-style type system (but some ideas like generics have become common in mainstream languages as well). When a program passes a type check, this is a kind of automated proof. In some cases, this will be able to detect some errors (e.g. forgetting the base case in a recursion, or forgetting to handle certain cases in a pattern match).

    On the other hand, these type systems have to be kept very limited in order to keep them decidable. So in a sense, we gain static guarantees by giving up flexibility – and these restrictions are a reason why complicated academic papers along the lines of “A monadic solution to a solved problem, in Haskell”.

    I enjoy both very liberal languages, and very restricted languages, and both have their respective difficulties. But it's not the case that one would be “better”, each is just more convenient for a different kind of task.

Then it has to be pointed out that proofs and unit testing are not interchangeable. They both allow us to put bounds on the correctness of the program:

  • Testing puts an upper bound on correctness: If a test fails, the program is incorrect, if no tests fail, we are certain that the program will handle the tested cases, but there may still be undiscovered bugs.

    int factorial(int n) {
      if (n <= 1) return 1;
      if (n == 2) return 2;
      if (n == 3) return 6;
      return -1;
    }
    
    assert(factorial(0) == 1);
    assert(factorial(1) == 1);
    assert(factorial(3) == 6);
    // oops, we forgot to test that it handles n > 3…
    
  • Proofs put a lower bound on correctness: It may be impossible to prove certain properties. For example, it may be easy to prove that a function always returns a number (that's what type systems do). But it may be impossible to prove that the number will always be < 10.

    int factorial(int n) {
      return n;  // FIXME this is just a placeholder to make it compile
    }
    
    // type system says this will be OK…