4 ms·

Humans tend to make more mistakes. Convincing, say, Coq's typechecker of your proof is stronger evidence of correctness than convincing yourself.

• pron 11y ago
  It is possible to prove program correctness -- by a computer -- that doesn't involve the type system.
  • eru 11y ago
    Depends on your definition of type system. Anyway, what methods did you have in mind?
    • pron 11y ago
      Any of the model checking methods (abstract interpretation etc.). The real life example I like to give is the detection (and correction) a few months ago of the bug in TimSort, possibly the most widely used sorting algorithm in the world (since its inclusion in Java in 2011). It was found using symbolic execution, and I'd like to see a programming language that is able to both express the algorithm in its efficient form (it is only used because of its speed) and prove its correctness using the type system in a way that is any easier than how it was actually verified.
      • tome 11y ago
        If you stretch the definition of type a bit, any expressible property of your program (such as "this function sorts list") is a type and anything that allows you to automatically prove those properties is a type checker. OK, actually a lot!