Lambda the Ultimate

Verified Programming in Guru is a tutorial introduction to Guru:

GURU is a pure functional programming language, which is similar in some ways to Caml and Haskell. But GURU also contains a language for writing formal proofs demonstrating the properties of programs. So there are really two languages: the language of programs, and the language of proofs.

In comparison to Coq:

GURU is inspired largely by the COQ theorem prover, used for formalized mathematics and theoretical computer science, as well as program verification. Like COQ, GURU has syntax for both proofs and programs, and supports dependent types. GURU does not have as complex forms of polymorphism and dependent types as COQ does. But GURU supports some features that are difficult or impossible for COQ to support, which are useful for practical program verification. In COQ, the compiler must be able to confirm that all programs are uniformly terminating: they must terminate on all possible inputs. We know from basic recursion theory or theoretical computer science that this means there are some programs which really do terminate on all inputs that the compiler will not be able to confirm do so. Furthermore, some programs, like web servers or operating systems, are not intended to terminate. So that is a significant limitation. Other features GURU has that COQ lacks include support for functional modeling of non-functional constructs like destructive updates of data structures and arrays; and better support for proving properties of dependently typed functions.

The tutorial is worth a read to anybody new to this style of programming as it is one of the most gentle introductions to dependent types and automated program verification that I've seen.

A Functional I/O System (or Fun for Freshman Kids), by Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. ICFP 2009.

Functional programming languages ought to play a central role in mathematics education for middle schools (age range: 10­-14). After all, functional programming is a form of algebra and programming is a creative activity about problem solving. Introducing it into mathematics courses would make pre-algebra course come alive. If input and output were invisible, students could implement fun simulations, animations, and even interactive and distributed games all while using nothing more than plain mathematics.

We have implemented this vision with a simple framework for purely functional I/O. Using this framework, students design, implement, and test plain mathematical functions over numbers, booleans, string, and images. Then the framework wires them up to devices and performs all the translation from external information to internal data (and vice versa) -- just like every other operating system. Once middle school students are hooked on this form of programming, our curriculum provides a smooth path for them from pre-algebra to freshman courses in college on object-oriented design and theorem proving.

This is a paper explaining some of the technical underpinnings of the How to Design Worlds curriculum that the PLT group has worked on.

I was tempted to categorize this as "functional", but decided against it. One of the really nice features of this curriculum is actually its applicability to imperative programming. Here, students are taught to think of interactive programs as functions written in world-passing style, and to specify programs in terms of the invariants that the function maintains on the world data.

That is: students are taught about loop invariants, without ever having to write an explicit loop. In my experience, loop invariants are the most difficult part of explaining Hoare logic (and hence of explaining imperative programming), because they require imagining a dynamic picture of what the static source code will eventually do. This style of teaching helps to manage that difficulty by making the dynamic state into visible animations.

The Simple programming language is a BASIC dialect for the Android platform highly influenced by Microsofts's pre-dot-NET Visual Basic.

In the 90s, a big company from up north was extremely successful with a dialect of the programming language BASIC (acronym for Beginner's All-purpose Symbolic Instruction Code). One of the reasons it was so successful was that the language was easy to learn and use.

Bringing an easy to learn and use language to the mobile world and the Android platform is the goal of the Simple project. Simple is a BASIC dialect for developing Android applications. It is particularly well suited for non-professional programmers (but not limited to). Simple allows programmers to quickly write Android applications by using the components supplied by its runtime system.

Similar to its 90s relative, Simple programs are form definitions (which contain components) and code (which contains the program logic). The interaction between the components and the program logic happens through events triggered by the components. The program logic consists of event handlers which contain code reacting to the events.

In a Qilang mailing list email Marker Tarver, creator of Qi, says

In a month I will be packing to go to India; this time for an extended
period. But its also a goodbye to Qi and computing. At some point
you have to acknowledge that Qi doesn't pay its way. It was fun
though and I'm not sad about it.

Qi has been a journey that began nearly 20 years ago when I was a very
different person and worked for a university. But the book on Qi II
marks a natural watershed. I need to move on. By September I will be
gone.

Energy-efficient computing is important in several systems ranging from embedded devices to large scale data centers. Several application domains offer the opportunity to tradeoff quality of service/solution (QoS) for improvements in performance and reduction in energy consumption. Programmers sometimes take advantage of such opportunities, albeit in an ad-hoc manner and often without providing any QoS guarantees. We propose a system called Green that provides a simple and flexible framework that allows programmers to take advantage of such approximation opportunities in a systematic manner while providing statistical QoS guarantees. Green enables programmers to approximate expensive functions and loops and operates in two phases. In the calibration phase, it builds a model of the QoS loss produced by the approximation. This model is used in the operational phase to make approximation decisions based on the QoS constraints specified by the programmer. The operational phase also includes an adaptation function that occasionally monitors the runtime behavior and changes the approximation decisions and QoS model to provide strong QoS guarantees.

The basic approach is not specific to energy considerations, and is basically based on placing approximation code based on profiling data. Energy is measured by sampling current and voltage from the main power cable.

It is nice to see programming language ideas being put to use to help protect the environment...

The system was implemented using the Phoenix compiler framework.

Sun has a new article out that talks about the changes in the upcoming JDK 7 to support dynamic typed languages. Of special note is the new invokedynamic bytecode:

the invokedynamic bytecode instruction enables an implementer of a dynamic language to translate a method invocation into bytecode without having to specify a target type that contains the method. The method specification in this case is a simplified constant pool reference, which specifies only a method name and type descriptor. The descriptor specifies the return type of the call and the type of method arguments.

Full article: New JDK 7 Feature: Support for Dynamically Typed Languages in the Java Virtual Machine

Past discussion on invokedynamic here and JAOO 2005 slides by Gilad Bracha.

Found via Wadler's blog: PLATEAU is calling for papers on the HCI side of PL theory, design, and tooling.

Programming languages exist to enable programmers to develop software effectively. But how efficiently programmers can write software depends on the usability of the languages and tools that they develop with. The aim of this workshop is to discuss methods, metrics and techniques for evaluating the usability of languages and language tools. The supposed benefits of such languages and tools cover a large space, including making programs easier to read, write, and maintain; allowing programmers to write more flexible and powerful programs; and restricting programs to make them more safe and secure.

Yep, it's that time of the year again: It was nine (!) years ago that LtU was born.

As is my wont, I am going to use this opportunity to say a few things in lieu a real life birthday party speech. Those of you with an historical bent may enjoy browsing the full set of birthday posts. Here they are: year one, year two, year three, year five, year six, year seven and year eight.

First, an apology. I am feeling a little guilty posting this, since I didn't post many substantive posts this year. I am still busy doing many things not directly PL related (such as this), and so have little to contribute. I prefer to lurk a bit and let others carry the burden (on this more, in a minute). I posted less home page items and more the discussion group this year, I think.

I find it hard to post as just one of the guys, a regular member of the community, however. Several times I made non-admin remarks about posts that I felt were not on topic for LtU, or - indeed - posted marginal items to the discussion group myself, only to be rebuked by many for misusing my authority or applying policies heavy handedly... So let me take this opportunity to respond from the pulpit... LtU relies on community moderation of posts. This was the mechanism we arrived when the issue of discussion quality came up. All the discussions about this are in the archives. There is no cabal. The solution was simple: members are expected to raise their concerns about problematic posts publicly, so problems and disagreements can be hashed out. Unless I or Anton post a message clearly marked as an "admin" note, which happens fairly rarely, my posts about policy issues have no more weight than those of any other regular member of the community. However, keep in mind that if I am rebuked, many others may conclude that they should refrain from voicing concerns and simply move to other sites. So instead of rebuking me when I voice my opinion - voice yours when messages are problematic (and when messages are particularly useful as well!). If you don't take care of LtU no one will.

So, the "bad news" is that many old-timers didn't carry their burden of policing, and some discussions may have suffered because of this. The "good news" is that this allowed more people to join the discussion. Not only new members (and people are signing up daily) - many people who have been lurking, sometimes for over a year, started posting regularly. This is great! Not only did this add great content, and move the discussion in new directions, it was really nice to see accounts that I presumed were dead come to life. Bet you know what's coming now, right? People who post regularly to the discussion group and think they can contribute to the home page are urged, as always, to let me know so I can make them contributing editors (that's the LtU parlance for members who post to the home page, nothing more; don't be intimidated by the title - you can post as infrequently as you want).

Another nice thing happened this year in terms of members contributing their efforts to the community. A few people volunteered to help deleting spam and spam accounts. I am not sure they want to be identified, but my thanks goes to them. I think we don't need more help on this front for the moment. Still, members should know that new spam accounts are created (and squashed) daily, and that this happens due to the efforts of several members besides the usual suspects.

The LtU "trademark" spread its wings a bit, from they days when LtU was just this blog. This happened without my involvement. Two things worth mentioning come to mind, but let us know if I forgot something important. There is a CiteULike LtU library (originally proposed here), and the a LtU twitter account (see here).

Indeed, it seems many LtU members have flocked to twitter. I am there (@ehud/@biocomputing), but as a late comer I don't have many LtU followers. Others who are better connected may speak up if they want... I am not sure if this a a good thing or a bad thing for LtU, but I guess it was bound to happen. Contributing editors should remember that LtU expects each man to do his duty and post new stuff here first!

Our tenth anniversary is coming up soon. How are we going to celebrate? LtU is a virtual community so maybe a virtual celebration is in order. Maybe we should think about planning a virtual event of some sort or another (guest bloggers, an online conference, or some other crazy idea). Alternatively, we may try to see if we can do something non-virtual... I've always found unconferences to be an appealing idea. Or maybe just LtU beer sessions around the globe... If anyone wants to pick up the glove and organize something, I am sure many here will be delighted.

Thanks again everyone. Let the nine-year long discussion continue!

P.S
I almost forgot... We had a very successful April Fools prank this year...

Robert Hieb, R. Kent Dybvig, and Carl Bruggeman. Representing Control in the Presence of First-Class Continuations. ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, June 1990.

Languages such as Scheme and Smalltalk that provide continuations as first-class data objects present a challenge to efficient implementation. Allocating activation records in a heap has proven unsatisfactory because of increased frame linkage costs, increased garbage collection overhead, and decreased locality of reference. However, simply allocating activation records on a stack and copying them when a continuation is created results in unbounded copying overhead. This paper describes a new approach based on stack allocation that does not require the stack to be copied when a continuation is created and that allows us to place a small upper bound on the amount copied when a continuation is reinstated. This new approach is faster than the naive stack allocation approach, and it does not suffer from the problems associated with unbounded copying. For continuation-intensive programs, our approach is at worst a constant factor slower than the heap allocation approach, and for typical programs, it is significantly faster. An important additional benefit is that recovery from stack overflow is handled gracefully and efficiently.

Many Scheme implementations do not implement call/cc particularly well, but it is important to remember that call/cc is not inherently slow. This is the classic paper describing a clever run-time representation that supports call/cc efficiently.

A blog post announces that some of the source code for the Apollo 11 spacecraft has been put online.

On this day 40 years ago, Neil Armstrong and Buzz Aldrin became the first humans to walk on the Moon. This was quite an achievement for mankind and a key milestone in world history.

To commemorate this event the Command Module code (Comanche054) and Lunar Module code (Luminary099) have been transcribed from scanned images to run on yaAGC (an open source AGC emulator) by the Virtual AGC and AGS project.

Since we LTUers spend a lot of time talking about the highest of the high level languages it's illuminating to see how much was done with so little. The source also shows that flying to the moon is really not that different from the kind of programming most programmers do every day. Note the comments.

VRTSTART	TS	WCHVERT
# Page 801
		CAF	TWO		# WCHPHASE = 2 ---> VERTICAL: P65,P66,P67
		TS	WCHPHOLD
		TS	WCHPHASE
		TC	BANKCALL	# TEMPORARY, I HOPE HOPE HOPE
		CADR	STOPRATE	# TEMPORARY, I HOPE HOPE HOPE
		TC	DOWNFLAG	# PERMIT X-AXIS OVERRIDE
		ADRES	XOVINFLG
		TC	DOWNFLAG
		ADRES	REDFLAG
		TCF	VERTGUID