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