philosophy-from-a-declarative-world.md 10 KB
title: Philosophy from a Declarative World date: 10 Feb 2017 ...
After years of programming in imperative languages like C and functional languages like Scheme, you have to wonder if there is something better out there. What follows are far out ideals for how a future language might be built.
Musings on Type Systems
Everybody in CS seems to love arguing over type systems. Static vs dynamic, explicit vs inferred, polymorphism, you name it. Get a Haskell programmer, a Lisper, a C coder, and a Pythonista in a room together -- I'll grab the popcorn! Yet, despite the strong opinions, it is easy to lose sight of why types matter in the first place: types are guarantees on otherwise chaotic program behaviour.
In other words, types are tiny proofs about the programs. In an explicitly
typed language like C, the programmer really is explicitly making (provable)
assertions about the code. For instance, I might write uint32_t cakeCount,
which can then be interpreted as a guarantee that the value of cakeCount is
in ${ x | x \in \mathbb{Z}, 0 \leq x < 2^32 }$. Why is this (rather verbose)
guarantee useful? To a human, it's probably not. But for the compiler it now
means that cakeCount can legally be stored in a 32-bit register. Perhaps that
isn't terribly interesting, since most compilers can avoid the underlying
mathematics for a simple example like this in practice. But it does mean that
a static analysis tool can guarantee, for instance, that iterating with the
eat method cakeCount times will always halt.
Really, there are two major implications to which a type system leads: better performance and provable correctness. It is useful to consider both separately, though the latter is rarely discussed outside of academic circles, and academia is only concerned with asymptotic performance! Nevertheless, for performance concerns, these "constraint-style" proofs are sufficient, e.g.: prove that the variable X will always fit in the register Y. For correctness, the proofs are somewhat more assertive in nature, e.g.: prove that the return value of the function F will always be a perfect square. The latter proof is clearly more difficult than the former, but I digress. The bottom line is, it would be wonderful if a computer algebra system could replace Hindley-Milner!
Unfortunately, arbitrary proofs about programs are subject to all sorts of issues which I alluded to above. If I could prove anything, why not, for instance, prove that an arbitrary program will always halt? Nevertheless, the Halting problem only Turing-complete languages (which includes everybody's favourites). In principle, it should be possible to design a non-Turing complete subset of one of the above languages, subject to limitations such as a guarantee of halting in a given time, perhaps these proofs are feasible. And sometimes that magic subset is all you need.
Magic Metadata
Natural language programming is many programmers' dream. In constrained situations, it is possible, for instance used in Wolfram Alpha among others. But for everyday work, it is still far-fetched and awkward; the primary issue is simply that natural language is ambiguous. Trying to have a computer derive meaning out of a textbook or a coder's comments is fruitless (at least until the singularity). Nevertheless, while even a specification can be ambiguous (much to the frustration of the hackers who implement it), they contain certain metadata that is objective. Perhaps the metadata is objectively more useful than the text itself!
Ultimately, natural language processing is focused on deriving meaning out of words, which for the moment isn't feasible, even on the rigid specifications associated with "enterprise-grade" software. But they feature something else: tables, flow charts, equations, and so on and so forth. The exact flavour of the supporting visuals varies greatly between fields, but they are usually quite thorough, with an elegance no amount of words (or traditional code!) could express. And many of these extra bits do map clearly to code.
If you take this idea of mapping metadata ad extremum, you might end up with a family of visual DSLs. LaTeX math might map to the expression computing the described value. A flowchart diagram written in Dot might generate a finite-state machine. A table of registers from a chip data-sheet might generate a set of macros. Even business logic can often be decomposed into these components. So much of a given program can be automatically generated from these Turing incomplete, semantic, often verifiable, embeddable languages. Even if the goal isn't to eliminate the code to begin with, so much of the application can be gutted out for scrutiny by non-programmer experts. And if nothing else, there is something decidedly satisfying about flow charts and nice typography!
Now Available as Markdown at a Website Near You
We live in a world with an Internet bought out by commercialism and almost entirely consumed by consumerism. Websites are bloated ("by necessity") with ads, trackers, flashy styles, invasive JavaScript, and so on. Try browsing the web with lynx -- I think you'll quickly agree that there is an issue. I shudder to think how these websites render with screen readers. Minimalism, a philosophy I used to endorse whole-heartedly for lack of better options, likes to push back by simply removing everything that's not directly relevant. It's an honorable idea, but there's a better way, once the underlying problem is identified.
Really, this is about taking control over presentation away from publishers and into the hands of users. Users should be the ones who set the CSS they want, rather than being forced to accept flashy styles. Users should decide how to aggregate content, rather than being forced to read about eleven weird tricks doctors hate (you won't believe number seven!). And perhaps most importantly -- although most controversially -- users should decide if, when, how, and how much to pay the author. Net neutrality goes a lot farther than ISPs.
I don't pretend to have the solution to this; after all, it is a social problem rather than a technical one. But to this end, I'm making my HTML and my style sheets purely optional -- every page on this website as of the time of writing is available directly as pandoc-flavour markdown. After all, as a writer my words matters more than any of the bling. Try it!
A Declarative World
My favourite programming language is markdown -- this post is written in it, in fact! For plain text, it is what-you-see-is-what-you-get (WYSIWYG), and for formatted-text, **it** is *natural*. It isn't without its faults, of course; the image syntax is understandably incomprehensible. But at the end of the day, it does what it claims to do, and it does it well.
Another language (or notation) I like a great deal is the language of mathematics. Again, it is not without faults; I maintain whoever chose^[OK, I know, I know, language and notation are evolved, not chosen..] the notation for formal logic and set theory had a vendetta against students. But for the most part, it is clean, mostly unambiguous, and usually legible. There are still, of course, movements trying to change the notation, like a personal favourite of mine, Tau-ism, and I concede that the meaning is rarely obvious when first learning the notation. Indeed, Bret Victor quipped that mathematics "should not be restricted to those with a freakish knack for manipulating abstract symbols". He might be right, although that issue is largely tangential here. (Get it? Tangential). Nevertheless, for what it does mathematical notation is nice -- and more importantly, it doesn't concern itself with what the engineer in me would call "implementation details". Elegance rules -- correctness is a close second with some of us!
Another paradigm with which most people are familiar is flow charts. They are visual representations of the control flow of a constrained program. If you want to sound smart at MIT parties, the fancy computer science term for this is a finite-state machine (FSM). Computationally, they are rather powerful, and for many people, they are intuitive.
So, many of you might interrupt me now, pointing out, "Alyssa, none of these are programming languages!" Indeed, these 'languages' are non-Turing-complete, non-programming, non-general, and at this point you might interject, "non-useful". In a sense, these languages are closer to data, capable of being interpreted by a human or by a machine. I feel this is a deeper idea than the von Neumann equivalency between code and data, since I'm not arguing that this is code. In any event, however constrained these "languages" may be, they might just be what a person wants.
Too often, in our "ooo, shiny" culture, we settle for more. But from my perspective, mathematicians want maths notation, not numpy. Writers want markdown, not HTML, CSS, and JavaScript. I'm not really sure there are people who want flow charts, but hey! Point is, enjoying programming is fine as a pastime, but it should not be the prerequisite for a user to control their computer. Luckily, as I said, most of the time programming is not necessary, only data.
I have a vision for a more declarative (digital) world. Websites should be written in markdown, not HTML, CSS, and JavaScript. Scientific algorithms should be published as an annotated specification, not messy programs in a mess of high-level programming languages and complex supporting libraries. And most of all, end-users should have the flexibility to participate in the development of the software they use, something that currently has a massive barrier to entry. Death to C, death to Lisp, and most of all death to JavaScript. We can build a more declarative world.