My Premonition

Last summer I got the opportunity to work briefly with Conal Elliott in Belgium. The two weeks I spent there are still making an impact on me; immediately I resonated with his semantic design idea. But the more important ideas were the ones I picked up subconsciously, and I’m just now becoming able to put them in words.

(1) If extreme idealism isn’t working out for you, maybe it is because you are not wholeheartedly following your own ideals.

(2) You must be the change you wish to see in the world (– Mahatma Gandhi). As applied to software: design software as if it were the beautiful paradise you want it to be, then build pieces of the scaffolding back to the status quo.

Both of these were key insights leading me to undertake Dana.

At the time I was desperately trying to create an FRP framework for Haskell, trying in terms of IO and STM and playing messy tricks with the operational semantics of thunks. It felt like cheating. I had the desire to throw away IO altogether in my efforts, just to see where that led me (this forced me to put aside the way I thought an FRP interface should look). This was an instance of (1).

But in Haskell, IO would always be beneath it all. Your functional program always becomes an imperative program at the end of the day. Maybe this dissonance is what is causing the endless FRP difficulties. Maybe we can’t really know what pure FRP is until we have pure turtles all the way down — until there is no impedance mismatch between the functional and the imperative. This set me on researching the idea of a purely functional operating system, which is still the slogan by which I name Dana.

But now Dana is more than that. Now, it is my (2). In this post, I describe how I see the world of software in 30 years. This isn’t about what kind of devices computers will be embedded in or how they are connected; this is about the process of developing software.


Code and program are the same; any fragment of code may be used interactively. Complex programs are just compositions of simpler ones, and composition of programs is a fundamental concept to both users and programmers. Thus power users cannot help but to be programmers.

Computer science has become a strict subfield of applied mathematics. Creating complex software is primarily modeling: the fundamental task in software development is to create a mathematical model of your problem. The model is encoded directly, and then software scaffolding is built around it, verified to the model. Reasonable shops do not dare ship code that hasn’t been verified to correspond to their model.

Development tools — programs that talk about programs — are astoundingly rich and expressive. Simply enter a property about your code. The tool goes off on a model search to try to refute the property. Meanwhile, in a way that my mind cannot yet comprehend, the programmer communicates the “essence” of why the property should be true, and the tool fills in all the details of the proof. The property is added to a database of facts, which everyone can immediately see and use.

Provably correct code is what people do, because the tools have made it so easy that it is an obvious engineering choice (this ease does not come without a resculpting of our brains). Gargantuan test suites are replaced by a few hours of a developer with a proving tool (an exponential increase in productivity came from the fact that theorems compose, but tests don’t).

User interfaces are mostly an artistic task, quite different from the rigorous visualization that modelers do. All objects have a few obvious ways to endow them with primitive user interfaces (see Eros). Then making a nice user interface is a matter of rearranging them, composing inputs and outputs, and drawing/animating things (under the assumption that computers are still monitor, keyboard, and mouse driven — make the appropriate generalizations).

The shops that will be renowned by power users are those who have a great program with a great interface, but they also ship components to the underlying logic. This is trivial for them, because of the ubiquitous separation between interface and logic. Some are still irrationally afraid of giving away their trade secrets by exposing this, so there are still lame, interface-only programs. But these lame programs will not have the chance to participate in the miracles of engineering the decade will bring, a combiatorical build up of the the work of millions of developers, coming together to create the Star Trek computer — or something else, far more advanced.


Computation is an information science, and is subject to the exponential explosion that comes with it. This Utopian vision hinges on correct composition of everything, from programs to facts.

Right now, software is primarily non-compositional. We have libraries and languages, which are built up of smaller libraries and languages. But end products are not designed to be composed; they are mostly designed for the end user only. But the end user is where the money is, thus where a great deal of the effort in the industry is going. Moreover, for advanced programs (say, Maya), the end user is also where a lot of the skill and talent is.

We have to work at this. There is little small-scale economic incentive to make your program composable; you just give your competitors the ability to use your software without you being able to use theirs. And it’s hard for idealistic young CEOs to try such a thing, since the state of software development means you have to put in a lot of work both to make your program composable and to compose other people’s programs. But these things are not fundamentally hard, they are just hard using the languages and methods of today.

Dana is my own first step in this direction. It aims to be an environment which forces everything to be composable and verifiable. This comes at the expense of mental laziness: you will have to seriously rewire your brain to work in it. I don’t believe that the enlightenment can come without this rewiring. I’m desperately trying to rewire my own, to even consider the choices that will be obvious to the generation ahead.

Is your brain going to be ready when the revolution comes?

About these ads

9 thoughts on “My Premonition

  1. May be your prophecy will become a reality.
    May be in 30 years, may be in 300 years.

    Seriously, i think computing is one of the most conservative sector. One reason is, outside academia, change is not driven by engineering and innovation. This language drives the unix-boom, this language is the system standard for the 30 years to come. This language drives the dot-net boom, this language is the net standard for the 30 years to come.
    No matter how beautiful our little designs are, what matters to the grander world is killer applications and money makers. And i don’t see it change in the 30 years to come.

    On more point, user as an educated person participating in the software world is the idea of Smalltalk and ETH-Oberon. No matter how great is the experience with them, they are both an unmitigated public failure. Your utopia sounds much like a Smalltalk environment on Haskell/Coq steroids. Seems actually pretty old to me. Smalltalk and Oberon proponents did not failed because they were not wholeheartedly following their own ideals. They failed because the world has followed the money and the trends, not the ideals.

    I still wonder what Dana is, it sounds more like a life-project than a product. No matter what, i wish this blooming exponential creativity becomes part of your (and our) future.

  2. I’m flabbergasted! Also envious. The kind of idealism I wish fueled me when I was younger.

    @SpiceGuid

    I take your points about Smalltalk and Oberon being unmitigated failures. Maybe they were just too advanced for their time, the same fate lying await for Dana.

    But the gorgeousness of composability is just too arresting to not do otherwise. If only there were more luqui’s who perceive this, if not actually all fired up to get their hands dirty. How else are we going to reach the stars?

  3. @SpiceGuid

    You’re both right and wrong. Languages like C and Java are indeed the work of a plodding mediocrity, but that does not mean all change moves at such a glacial pace. PHP took the web world by storm, and though it’s moribund it paved the way for others like Rails. Python took the scripting world by storm and is now an entrenched standard which will be with us for a while to come. Ruby took the scripting world by storm and ain’t near dying yet. Haskell has escaped academia and seems to be preparing to make a run of it. JavaScript has grown up and is taking something by storm, though I’m not sure it knows exactly what.

    Idealistic languages like Smalltalk, Oberon, Oz, Lisp, (Haskell?), and Prolog have had less public success, but I’m not sure that can be blamed on the idealism per se. We don’t explain the revolutions of the past twenty years by some special property of “scripting” which makes it different from “systems” and allows revolution to be more frequent, so why should “idealism” be special? Idealistic languages often suffer the problem of not following through with their ideals (e.g. cut in Prolog, unsafePerformIO in Haskell) or of not being able to explain the ideals quickly in a way that is understood (Smalltalk: “really everything is really an object”, Oz: “dataflow variables come from the future”, Lisp: “Macros are functions that aren’t functions and aren’t macros either”, Haskell: “a monad is a warm fuzzy thing”,…).

    Inertia in programming is inevitable. The Linux kernel, the Apache webserver, any compiler, GTK or Qt— these things are artifacts which represent an enormous store of work. Since we already have them, the artifacts themselves must become obsolete before the languages they’re written in can become so. Someone has to translate the man-years of accumulated knowledge in these artifacts into whatever new language, and it is this work that causes the inertia— not the recalcitrance of CEOs, a love of old languages, or any of the other bugbears so oft cited.

  4. “Is your brain going to be ready when the revolution comes?”

    Probably not. Meanwhile, it is important to find out which is a good programming language for MasPar AI, Haskell or Erlang or something else.

  5. My (current) fantasy:

    Code is evaluated as I type. All code is conceptualized as assertions. The way current IDEs evaluate type assertions as I write them down, so that I know immediately when there is a typing contradiction, is seen as an old and incomplete way of doing this. As soon as the system notices a contradiction between two of my assertions (or perhaps between my assertion and system-level assertions, or my assertion and an assertion in a library) it notifies me, requiring me to mediate the conflict.

    Even if I only provide enough assertions to specify the *model*, the code can start to do its job; just slowly, via brute-force deduction. Execution is made faster by providing lemmas, and/or by providing extra assertions about how deduction should proceed.

    Object-oriented style is seen as the tactic of providing assertions about the abstract data structures directly, rather than only making assertions about how the program proceeds.

  6. @SpiceGuid: Smalltalk has been covertly influential on a lot of computer science. The object models of ruby and perl both at least mention smalltalk in their inspirations. And despite Squeak’s “failure”, it has at least been influential and inspiring to me.

    The way a language drives a boom is by being good at something. I wouldn’t want the proof paradise to come about unless it had real, tangible engineering advantages. I happen to believe that proofs will far outperform unit tests (which are booming just now), once the infrastructure is there to support them. The same argument applies for uniform composability.

    Obviously the post is an instance of (2). I’m being idealistic and optimistic, because without unrealistic zealots like me and Conal, the future I described has 0% chance of happening.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s