This talk is about hacking mathematics. I will try to give you guys an intuition behind formal logic and some cool things such as Curry-Haward isomorphism and Godel's incompletness theorem. I will show you what theorem proving is all about and why every one of you who has ever run GCC has already done plenty of theorem proving in their lives. This is not, however, a formal talk, and I've skipped a lot of details to make the material penetrable to an average l33t C hacker, so please don't shoot me if you know about this stuff and notice little lies in my talk. There's a few of them, but the basic idea is that, at the end, you will be able to go on Google (Wikipedia comes highly recommended!) search for all this stuff and find out all the nitty-gritty details for yourself. A few years ago I've attended a talk by Philip Wadler and, I've been using formal systems for years back then, but only during that talk Philip mentioned some insignificant thing about encoding of falsehood and it all “clicked together”: I got a zen-like light hit me from above and everything was clear and simple and beautiful. So I'm hoping this talk will give some of you a similar effect; the rest of you better have some panadols in your conference bags, because tonight you'll be nursing a massive hangover - and I don't mean from the conference dinner.
It is well-known that the document typesetting system TEX is a Turing-complete language, and, as such, may be used to solve arbitriary programming problems. Many TEX users who have been exposed to the design of LaTEX packages even realise that hacking in TEX may be useful. It is a well-kept secret of the TEX elite (TEXperts) that it is also a lot of fun.
It is the purpose of this paper to explain the mechanics of using conventional programming structures in TEX, while exposing the utility of writing TEX programs, in a hope of initiating a few of its readers into the inner circle of TEX addicts.
The author of this paper has written a number of
TEX programs himself,
including K-Fish
and lambdaTEX,
a popular pretty-printing package for the functional language Haskell,
written entirely in over 3000 lines TEX
code. By working directly in TEX,
lambdaTEX allows authors to incorporate
neatly-typeset fragments of programs in
LaTEX documents simply
by pasting the code into an appropriate \begin{}..\end{}
environment block, without resorting to any external preprocessing
tools or heavy manual annotations, or putting up with the
ugliness of code typset with the verbatim environment.
The indented audience of this paper are UNIX programmers who: (1) enjoy hacking and (2) use TEX or LaTEX to typeset technical papers containing programming code and (3) really, truly love hacking.
Few people realise that, from the language-theoretic point of
view, TEX belongs to the lazy
continuation-passing family of programming languages, which includes a
few other popular languages such as Standard ML, Lisp and Scheme.
Continuation passing style (CPS) has been successfully employed in the
theoretical computer science community to model and implement
sophisticated language features such as exceptions and concurrency.
In C, a primitive form of CPS is available in the form of
setjmp and longjmp. The paper explains this
style of programming in terms that should be comprehendible to any
competent hacker, even without a prior background in functional or
declarative languages.
Once the continuation-passing style is understood, it is a small step to move from coding in ML to writing programs in TEX, and this paper will demonstrate how to make this step without requiring any prior knowledge of lambda calculus or functional programming.
Last but not least, it is a purpose of this paper to cultivate the old tradition of minimalistic hacking - doing the impossible with seemingly-inadequate tools, and, most importantly, having lots of fun in the process. In today's climate of a commercialization of the open source, it is worthwhile to look back to the days gone by, when public software was created only by hackers having fun over a cup of coffee.
The static single assignment (SSA) form is central to a range of optimisation algorithms relying on data flow information, and hence, to the correctness of compilers employing those algorithms. It is well known that the SSA form is closely related to lambda terms (i.e., functional programs) and, considering the large amount of energy expended on theories and frameworks for formal reasoning in the lambda calculus, it seems only natural to leverage this connection to improve our capabilities to reason about compiler optimisations. In this paper, we discuss a new formalisation of the mapping from SSA programs to a restricted form of lambda terms, called administrative normal form (ANF). We conjecture that this connection improves our ability to reason about SSA-based optimisation algorithms and provide a first data point by presenting an ANF variant of a well known SSA-based conditional constant propagation algorithm.