|
Another interesting freshmeat project:
Domino on Acid - Natural Deduction Visualized As A Game Of Dominoes
“Superficially this is a colorful variant of dominoes with weird tiles, a simple matching game to play during lunch breaks. But hidden behind this façade are the inference rules of natural deduction, so that every solved level represents a proof of a tautology. This program demonstrates that logical reasoning can be done without any language or symbols, relying purely on the brain's visual capabilities.”
It's rather fun to play around with, though it takes quite a while to figure out what's going on.
How does this relate to programming languages? By the Curry-Howard correspondence, every natural deduction proof corresponds to a term of the simply-typed lambda-calculus, extensions of which form the core for most typed functional programming languages. Thus, when you solve a domino puzzle, you are actually writing a program with a certain type.
| 
Domino on Acid
