I love to program in various languages, and I like to study (and often, comment upon) the various features (or lack) in these programming languages. I’m also very interested in Programming Language Metatheory, which I will informally define as the relationship between a programming language’s syntax, semantics, and purpose. This includes proof systems about program correctness. My formal training as a Computer Scientist was fun because I was able to learn an entirely different level of *programming* and an associated notation: the language of formal proofs.

One of the important characteristics I need from my blogging and authoring technology is the ability to express proofs, semantics and the notation necessary for theoretical computer science.

#### Definition of Programming Language

- A notation for giving instructions
- A notation for describing inductive structures
- A type system

#### Examples of Programs

##### A Java program

```
public class HelloWorld
{
public static void main(String[] args)
{
System.out.println("Hello, World");
}
}
```

##### Driving Directions

```
1. 2 blocks North
2. Left at Wilson Rd
3. East for 3 blocks.
```

##### Mathematical Transformation

The solutions of $$ax^2 + by + c = 0$$ are given by \eqref{eq:quad} below:

##### A Logical Proof

Hmmm. So the wonderful `bussproofs.sty`

that is used for doing Prawitz and Gentzen style proof trees is not available in my MathJax-enabled LaTex compatibility mode. This sucks, but also presents a wonderful opportunity in terms of implementing a better, more interactive proof display structure. I’m thinking AngularJS would be a great way to create directives that could contain expressions in LaTeX, but that would wield the layout engine of HTML5.

Meanwhile, I have some fragmentary attempts in displaying proofs below…

Let’s try a simple Gentzen Sequent, but without any tree notation:

$$ \def \fCenter{\vdash} $$

$$ B,\Gamma \fCenter A $$

$$ \Gamma \fCenter B\backslash A $$

Cool, that sort of worked. Now let’s try a sequent deduction. Here, the deduction in the Lambek calculus that from $$A/B$$ and $$B$$ we can conclude $$A$$ in the shared context $$\Gamma,\Delta$$.

The above deduction isn’t bad, and not too hard. But I didn’t get to annotate my line with a rule. Let’s try the next Lambek rule, where I’ll try to label the line.

Ugh. That doesn’t look right. The rule annotation $$[\backslash E]$$ is showing up on its own line and I cannot get it to play nicely with the `\hline`

.

I guess I can use two `\hline`

and place the rule annotation between them:

So here I’ll try to use the `\cfrac`

(continued fraction) capability:

$$ \cfrac {\Gamma \fCenter B \hspace{5ex} \Delta \fCenter B\backslash A} {\Gamma,\Delta \fCenter A} {\hspace{2ex}\scriptsize[\backslash E]} $$

Works nicely and places the rule annotation. Let’s see if it holds up with larger proofs (this is an incomplete proof of an obvious theorem; I have left out the variable introduction parts.)

$$ \cfrac {\Gamma \fCenter B \hspace{5ex} \cfrac {B \Delta \fCenter A} {\Delta \fCenter B \backslash A} {\hspace{2ex}\scriptsize[\backslash I]}} {\Gamma,\Delta \fCenter A} {\hspace{2ex}\scriptsize[\backslash E]} $$

##### Other examples of *Program*

Circuit Diagram

Rube Goldberg Machine

Musical Score

Cooking Recipe