Lambda the Ultimate

For a long time now, on and off, I've been writing a Lisp tutorial for regular programmers. The idea was not to explain intricate details of Lisp, but help people understand what exactly the nature of the language is, and why some of its features are great for modern software development.

I'm very interested in feedback so I can improve upon the tutorial and explain things people still don't understand. You can read it here.

Push 3.0 Language Description:

Push is a programming language intended primarily for use in evolutionary computation systems (such as genetic programming systems), as the language in which evolving programs are expressed. Push has an unusually simple syntax, which facilitates the development (or evolution) of mutation and recombination operators that generate and manipulate programs. Despite this simple syntax, Push provides more expressive power than most other program representations that are used for program evolution. Push programs can process multiple data types (without the syntax restrictions that usually accompany this capability), and they can express and make use of arbitrary control structures (e.g. recursive subroutines and macros) through the explicit manipulation of their own code (via a "CODE" data type). This allows Push to support the automatic evolution of modular program architectures in a particularly simple way, even when it Push is employed in an otherwise ordinary genetic programming system (such as PushGP, which is a "generic" GP system except that it evolves Push programs rather than Lisp-style program trees). Push can also support entirely new evolutionary computation paradigms such as "autoconstructive evolution," in which genetic operators and other components of the evolutionary system themselves evolve (as in the Pushpop and SwarmEvolve2 systems).

MathLang is next to what the name suggest: a mathematical language, also a framework for writing mathematical texts. It allows for more formalisation than the normal Common Mathematical Language does in such a way that one can check the correctness of the text (on some given level) but also convert it to even more stringent forms so that it can be checked by proof checkers such as (Mizar, Coq, PVS, etc.).

The Fortress Language Spec v0.933

There is now a chapter on the memory model (Ch. 18).

Again, this spec looks more tidy than its predecessors.
Evaluation, types, and operators have their own chapters now.

I consider myself an expert in imperative programming languages but I'm very green in the field of modern functional languages (I'd be better off alligator wrestling than writing monads, but I can still 'cadr' your 'cons'). Here is a quote from a well written post by Matt Helige ( http://lambda-the-ultimate.org/node/1455 ) which kept me up last night:

Things get more complicated (or is it simpler?) when you consider polymorphic types, like "α -> α" where α is a type variable rather than a concrete type. In a pure language with "parametric" polymorphism, there is only one function with this type. The word parametric in this context effectively means "type variables are black boxes": i.e., there's no way to say "if α = int, then..." or anything of that form. They're completely abstract. Once you see that, it's pretty easy to see that a type like α -> α can have only one implementation, or "inhabitant": since there is no conceivable way that the function can inspect its argument or construct a new value of the same (unknown) type, we can prove that any value with this type must be the identity function.

I didn't "see" what Matt was talking about until today. You have to realize that I think of C++ templates (and Java / C# generics) when I think about parameteric polymorphism. So I didn't understand where the restriction came from.

What had confused me was that in C++ the compiler does allow type choices by overloading template functions. Whether or not this is a "good thing" is probably debateable, so I figure why not debate it. Why or why not is C++ style parameterization where template T f(T x) {...} can legally have multiple implementations a good or bad thing?

Even though I am not completely sure if LTU is the appropriate place to discuss this paper by Yves Guiraud, I see no danger in posting it anyway.

Abstract: In this document, we study a 3-polygraphic translation for the proofs of SKS, a formal system for classical propositional logic. We prove that the free 3-category generated by this 3-polygraph describes the proofs of classical propositional logic modulo structural bureaucracy. We give a 3-dimensional generalization of Penrose diagrams and use it to provide several pictures of a proof. We sketch how local transformations of proofs yield a non contrived example of 4-dimensional rewriting.

It discusses higher dimensional rewriting for SKS a deductive system for classical propositional logic in the style of the Calculus of Structures.
In intuitive sense this article has had a great appeal on me and I did not want to withhold it from the rest of us.