Building Robust Systems (2008) [pdf] | Hacker News Reader

Building Robust Systems (2008) [pdf]

groups.csail.mit.edu

93 pointsmolteanu6 comments

There is this video[0] on the subject matter.

Isn't the premise a bit wrong? Sure Internet scaled, but with a lot of problems over time. Like any system, obviously, just pointing out that all big systems had big hiccups. Most engineering problems have fixed constraints, but in software those constraints are ever changing.

I love this paper.

I love this paper too.

> However, I am considering an even more general scheme, where it is possible to define what is meant by addition, multiplication, etc., for new datatypes unimagined by the language designer

So, um, like this?

    signature RING =
    sig
      type t
      val + : t * t -> t
      val * : t * t -> t
      val ~ : t -> t
    end

> Extensible generic operations are not for the faint of heart. The ability to extend operators after the fact gives both extreme flexibility and ways to make whole new classes of bugs!

This is precisely why parametric polymorphism is superior to ad-hoc polymorphism as a way to enable programs to work in previously unanticipated situations. Don't work with concrete use cases, work with the minimum abstract requirements that allow your program to work!

> On the other hand, some mutations will be extremely valuable. For example, it is possible to extend arithmetic to symbolic quantities.

So, for example, like this?

    functor PolynomialRing (R : RING) : RING =
    struct
      type t = R.t list
      
      fun xs + nil = xs
        | nil + ys = ys
        | (x :: xs) + (y :: ys) = R.+ (x, y) :: xs + ys
      
      (* define multiplication and negation too... *)
    end

I don't think that ML-style type systems address the fundamental problem that Sussman is trying to articulate in this note.

I'll try to explain.

Your definitions of Ring and PolynomialRing are incomplete because neither specifies the appropriate set of axioms. Because you do not specify those axioms, your type signature is underspecified. As Sussman puts it, "It is probably impossible to prove very much about [the] program" (at least, without inspecting the implementation itself).

To give a concrete example, the type signatures of Ring and CommutativeRing are the same in System F. And as Sussman puts it, "a program that depends on the commutativity of numerical multiplication will certainly not work correctly for matrices."

Now, this doesn't so much matter for human-written code, because us humans will implicitly fill in the details and never pass a mere Ring into an algorithm that expects a CommutativeRing, even if the two types are structurally identical. However, this does matter a lot if you want to use the structures of types (or their programs) to direct automated program mutation/construction.

And automated program mutation/construction is exactly the sort of thing that this note is about ("The most robust systems are evolvable").

Of course, there do exist type systems which fix this problem by allowing you to specify the axioms to which a Ring or CommutativeRing must conform. But using those systems is a crap load of work, requires a PhD's worth of effort to become efficient at, and of course now you have to do full-blown theorem proving. Which, IMO, introduce the same "brittleness" that Sussman talks about at the beginning of the essay". Data propagation and decorated values are Sussman's proposed alternative, from what I can tell.

So 1) it's true that type theory provides one solution to Sussman's problem. But that type theory is something much more expressive than System F. And 2) given the difficulty of using those systems (eg CIC) in practice, I think Sussman's proposed alternatives are worth seriously considering.

Reply on news.ycombinator.com