1. 8
  1.  

  2. 4

    It’s tempting to build this up into a case against type checking. I don’t want to do that. Often safety is so important that you want to have guarantees built into the code. But there’s something about doing the mental work to just know that what you’ve done is correct.

    An interesting chicken and egg type question is raised for me here. Are the benefits of types as appealing if you haven’t already felt the pain of having to be constantly meticulous — even paranoid — by working without them?

    Here’s the thing. We should know that our tests will pass before we run them. We should be right most of the time. The times when we are wrong? Well, we should really stop then and figure out what we were missing. Where did our mental model of the behaviour of the code diverge from the actual behaviour of the code? That’s the space where bugs happen.

    I like this approach. I think it even isn’t exclusive to programming. When I was a musician, I remember one exercise to improve your ability to express an idea through your instrument is to sing the phrase you’re playing at the same time as you’re playing it.

    1. 2

      Yes, I think a lot of these practices apply in other areas too. I wish I’d mentioned in the blog that you can do the same thing with the type checker. Before compilation, be sure that it will pass. When it doesn’t there’s something to learn.

      1. 2

        My most-recent proposal for people learning software development is an easy/safe language first designed for purpose, then a realistic one like Python/Go that’s still easy, and then something like C. Perhaps throw something between first and second option that has no safety at all. Might be first language with checks removed. Teacher tells them to solve tricky problems with no types or GC so they run into all kinds of problems. They experience the pain. Then, they’re shown later on how type and memory safety prevent those specific errors with what tradeoffs.

        What you think?

      2. 2

        In Limbo article:

        “All editing operations were transformations of the syntax tree. Surprisingly, about 100 operations sufficed to cover all common edits. What if the unit of change was the tree transformation?”

        Sounds like they’re about to rediscover a language from the 1950’s. Since LISP/Scheme, those concepts grew into more metaprogramming in general with first-class support for key methods of transforming programs. A good example is Rascal MPL. So, don’t stop at trees folks. Keep exploring! :)