1. 57
  1.  

  2. 6

    This is so cool that I’m nearly inspired to pick it up as a new hobby of my own! (Along with the other countless number of hobbies I have…)

    1. 5

      I do suggest checking out lightweight methods such as Alloy Analyzer or learntla.com first. Will give you a taste of that kind of thinking and possibly immediate benefits without the pain of heavy stuff. If you like that, then Software Foundations or Certified Programming in Dependent Types are books to check out.

    2. 4

      For me the holy grail would be to write a 5k LOC C program, that can be compiled with a regular C compiler, that has no bugs. Is that possible today?

      1. 6

        seL4 is over that plus has assembly. That covers first point. Ultra-hard work though due to C’s design or lack of. The second part is problematic due to (a) compiler complexity creating bugs and (b) optimizations creating even more. Csmith testing showed only CompCert came out with just a few bugs (spec errors, not code) with regular compilers having a pile of them.

        So, half-yes, half-no, and you probably wouldn’t want to. You’d be proud of you did it for a useful program, though.

        EDIT: Also, look up Verisoft project’s verified stack done in a C subset (C0). It was impressive but I cant recall lines of code in VAMOS microkernel and SOS OS.

      2. 1

        This week I was reading about the theoretical underpinning of recursive definitions: fixed points. Whenever you define something recursively, you are technically taking a fixed point of a continuous function (yes, you read that correctly!). There is some really cool math behind this called domain theory.

        Recursive definitions don’t need fixed points. c.f. Roza Peter Recursive functions. Recursion is a simple thing. It’s weird how people take pride in making the simple seem utterly complex. See https://plato.stanford.edu/entries/recursive-functions/ for a nice summary.

        1. 6

          Unless you want to implement recursive functions in a pure language. Because you need to have evaluated the function and bound the result to a name in order to bind the name when it occurs within the body, you have a bit of a chicken-egg problem. But you can use the Y combinator (which is really about finding fix points) and a modified version of the recursive function definition to achieve general recursion in a pure (read: lambda calculus) setting (of course, it is usually implemented with mutable cells, as far as I’m aware).

          It’s not “making something complex out of something simple”, it is an important part of the history of computer science, the discovery that allows Lambda Calculus to achieve general computation and be Turing complete.

          Getting into the complicated roots that gave rise to something simple != ruining something simple.

          tl;dr: being dismissive and elitist isn’t a good look

          1. 3

            Peter’s work is in mathematics, not programming languages. It is set in the context of an arithmetic approach to computability which is equivalent in expressiveness to the lambda calculus, but much more clear and simple. I wonder how much of the neglect of the Skolem/Peter line of work is due to a preference for complexity, and how much is due to Peter’s gender, but whatever the cause: in mathematics, it is possible to choose to define recursion from basic principles without getting into the complexities that grafting recursion on to lambda calculus entails. The way recursion works in programming languages is, in my opinion, better represented in terms of recursive arithmetic than in the lambda calculus. If you think of a computable function something that can be defined by an algorithm, the apparent paradox of recursion in LC evaporates.

            No criticism of the poster - that’s the orthodox point of view. But to me it’s a wrong turn.

            1. 2

              It would help in a rebuttal like this if you gave examples of people doing exactly what you’re describing. I imagine it’s been done if it’s much easier. Then, any readers more knowledgeable about math or formal methods might look into such things more. We might get another interesting post out of it.

              1. 1

                Recursion has been a known technique in mathematics for a very long time. It generally does not involve taking a fixed point on a continuous function and has nothing to do with “domain theory” except in very specialized circumstances. I think that the main result of type-theory/formal methods has been to create an obscure, specialist vocabulary.

                1. 1

                  Domain theory and fixed points on ωCPOs are only needed in the context of polymorphism. Simply-typed lambda calculus has set theoretic models, after all. I doubt very much that the “arithmetic approach to computability” treats polymorphism.

                  1. 2

                    That’s great. It is interesting that the approach taken to computability by Skolem, which is the primary basis of Godel’s proof, now merits skeptical quote marks!

              2. 1

                I wonder how much of the neglect of the Skolem/Peter line of work is due to a preference for complexity, and how much is due to Peter’s gender, but whatever the cause: in mathematics, it is possible to choose to define recursion from basic principles without getting into the complexities that grafting recursion on to lambda calculus entails.

                Does the Skolem/Peter line account for polymorphism and higher-order functions? If not then there’s no need for the conspiricy theories. They are where the tricky bits of of programming language semantics start, after all. Programming language theorists didn’t make their subject complicated just for the hell of it.

                1. 1

                  Conspiracy theory? Give me a break. The original claim was: “ Whenever you define something recursively, you are technically taking a fixed point of a continuous function (yes, you read that correctly!).”

                  If it had been: “Whenever you define something recursively in typed lambda calculus (or similar) , you are technically taking a fixed point “, I would not have commented.