1. 3
    Why is imperative programming so complex? plt quora.com
  1. 6

    In contrast, genuinely functional (“denotative”) programming makes it practical to prove programs correct and even calculate them systematically from elegant (simple, precise, and powerful) specifications.

    Most software in the marketplace is full of specification holes. The lack of adoption of formal methods in industry stems from the fact that fully specifying behavior early enough takes many times longer than using informal methods to work around an incomplete specification. Even those who do fully specify the requirements for software don’t tend to use formal methods because the precision resulting from formal methods is also an order of magnitude more complex to decipher when it comes time to change the specification. That doesn’t even get into the issue of stored data.

    1. 4

      Is there a particular thing on this page you wanted to draw attention to? I’m just seeing a basic quora page.

      1. 6

        Given the initial title, I believe srid meant to share this specific answer by Conal Elliott.

        1. 9

          Eh, don’t think this is really lobsters-quality. The specific answer is “Read this, also imperative programming isn’t rigorous because it isn’t.” Not much to discuss there.

          A few years back I ran a challenge to see if this was really true and the general results were that verifying FP programs wasn’t actually much easier than verifying imperative programs.

          1. 2

            Is there a repository that collects all the solutions to your challenge? I’d love to be able to compare them.

            1. 3
          2. 1

            Thanks, this is very interesting. I believe the differences between imperative and functional programming can mostly be rectified through the concatenative calculus, though. That’s essentially what I’m trying to do with Dawn. It requires a relatively complex type system, though. And it’s not clear how to integrate dependent types, which might be preferable for proofs. But I hope to eventually add proofs as a meta-languange.