Lambda the Ultimate

Formal proofs, especially in support of Mathematics, is not something that I work with - (I use a lot of intuition in analyzing my code). I found that the articles from The American Mathematical Society A Special Issue on Formal Proof are fairly good introductions to the subject of using Proof Assistants in Formalizing 100 Math Theorems.

Traditional mathematical proofs are written in a way to make them easily understood by mathematicians. Routine logical steps are omitted. An enormous amount of context is assumed on the part of the reader. Proofs, especially in topology and geometry, rely on intuitive arguments in situations where a trained mathematician would be capable of translating those intuitive arguments into a more rigorous argument.

A formal proof is a proof in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. All the intermediate logical steps are supplied, without exception. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive, and yet less susceptible to logical errors.

Though the articles are focused on the application to mathematical proofs, they do give a background on languages that are continually mentioned on LtU (HOL, Coq, Isabelle, etc...).

Hello.

I feel like I'm entering the lions den here, but for the past couple of years I've been working on an online book: Exploring Programming Language Architecture in Perl and I'd be very grateful for any comments, criticisms or suggestions on it.

It's purely a hobby project, not for profit. I feel that it may be pitched a little high for your average perl programmer, and it's far too "folksy" for a serious academic text, but I've had fun writing it and I learnt a lot in the process too.

So far it covers basic lexical closure, objects and inheritance, continuations, trampolining, and logic programming using failure continuations and backtracking. I plan to add chapters on garbage collection, types, and Compilation.

Please don't jump to conclusions from the first couple of chapters that it is a lame implementation of Scheme, I get to a proper cons cell structures and the like later on. The purpose of the first chapters is just to get a working interpreter in terms that the average Perl programmer can understand with little effort.

I freely acknowledge that it leans rather too heavily on the classic SICP and EOPL, hopefully I can remedy that in subsequent iterations.

I'm currently working a compiler (not yet on line) targeting a virtual machine also written in Perl. I fully realize that "my first compiler" is not a fit topic for a book, so I'll be throwing that away as a learning exercise and starting it again at some point.

Please be kind.