Lambda the Ultimate

Dear all, I often hear the claim that immutability and pure functions are easier to test. While I personally believe the idea, I was looking for some disciplined research on the topic. I was hoping to go beyond the usual "hearsay" of PL communities.

Any advice from the experts?

Axiomatic Language was mentioned on LtU long ago, but with our recent paper A Tiny Specification Metalanguage [Wilson & Lei, SEKE 2012], we thought a new post would be in order:

A logic programming language with potential software engineering benefit is described. The language is intended as a specification language where the user specifies software functionality while ignoring efficiency. The goals of the language are: (1) a pure specification language – “what, not how”, (2) small size, and (3) a metalanguage – able to imitate and thus subsume other languages. The language, called “axiomatic language”, is based on the idea that any function or program can be defined by an infinite set of symbolic expressions that enumerates all possible inputs and the corresponding outputs. The language is just a formal system for generating these symbolic expressions. Axiomatic language can be described as pure, definite Prolog with Lisp syntax, HiLog higher-order generalization, and “string variables”, which match a string of expressions in a sequence.

Axiomatic language requires solving the difficult problem of automatic synthesis of efficient programs from specifications. Is there any hope for this?

Peter Landin Annual Semantics Seminar

3 December 2012

BCS London Offices

First Floor, The Davidson Building

5 Southampton Street

London

WC2E 7HA

http://www.bcs.org/upload/pdf/london-office-guide.pdf

https://events.bcs.org/book/361/

Introduction
----------------

Peter Landin (1930--2009) was a pioneer whose ideas underpin modern computing. In the
1950s and 1960s, Landin showed that programs could be defined in terms of mathematical functions, translated into functional expressions in the lambda calculus, and their meaning calculated with an abstract mathematical machine. Compiler writers and designers of modern-day programming languages alike owe much to Landin's pioneering work.

Each year, a leading figure in computer science will pay tribute to Landin's
contribution to computing through a public seminar. This year's seminar is
entitled "Unifying Theories of programming" and will be delivered by
Professor Sir Tony Hoare (Microsoft Research).

Programme
----------

5.15pm Coffee

6 pm Welcome and Introduction (Professor Peter O'Hearn, UCL)

6.05pm Peter Landin Semantics Seminar:

Unifying Theories of programming

Professor Sir Tony Hoare (Microsoft Research)

7.20pm Close

7.20pm - 8.30pm Drinks Reception

Registration
----------

If you would like to attend, please register online:

https://events.bcs.org/book/361/

Seminar details
-------------

Unifying Theories of programming

Professor Sir Tony Hoare (Microsoft Research)

Two Classical Theories of programming are (1) the Hoare calculus of triples,
for proving correctness of sequential programs, and (2) the Milner calculus
of transitions, for specifying the intended execution of concurrent processes.
I have long thought of these theories as rivals. But I now realise that the axioms
of both these theories can be defined and proved in terms of the elementary laws
of programming. A new axiom called 'exchange' is provable from Milner's definition
of concurrency, and also justifies the newer rules for concurrency that have been
introduced in the Hoare Theory by separation logic.

In a nutshell, SPREAD solves the major problems we face when we try to manage Programs.

Solving the dependency hell

I wonder: why is it that spreadsheets appear to be ignored by real programmers?

Is it because spreadsheets are the equivalent of spaghetti code? Is it because spreadsheets are hacks, put together by non-savvy 'business' people?

The horror!

Yes, I admit. I also very much believe all this to be true. Spreadsheets are sloppy programs. Hence, we programmers don't want to bothered by them. At the same time, research shows that almost 5% of the spreadsheets contain serious errors, causing multi-million dollars of losses.

That figure should freak you out, if you happen to own a bank account. I know firsthand that our banks still run some of their critical businesses on broken spreadsheets. The same spreadsheets we programmers tend to ignore.

Sure, there are attempts to lift spreadsheets into the realm of functional programming, with Reactive Functional Programming (FRP) as the most recent development. But FRP doesn't feel right. As a programmer? May be yes. But I don't think the 'poor' people will understand. FRP is just to distant from their beloved spreadsheets.

Can we educate people to learn FRP? I don't believe we should. What I believe is that we must teach them appropriate 'programmer values':

Modularity
Expressivity
Repeatability
Testability
Control
Performance
Versioning
Continuous builds
Production runs
No crashes please

None of these can currently be attributed to legacy spreadsheets. Ultimately, that's why I think legacy spreadsheets are bound to be a failure. We need more programming, without getting in the way of 'getting things done'.

So that's our challenge: to enhance spreadsheets, so that programmers and business people will meet each other in cells. It is obvious that I've accepted this challenge: to develop a new powerful spreadsheet paradigm. A paradigm for everyone to like.

Edit: a small edit

May I draw your attention to the SPREAD programming language. It has not been implemented yet, but its design is almost finished.

SPREAD borrows from many programming languages, but also introduces a number of interesting new concepts:

1) Programs are first-class immutable values and are written in postfix format
2) Programs are built from Operators, Streams, Symbols and Characters
3) Programs may have alternative Versions - aka a Set of Programs
4) A Stream encloses a sequence of Programs, so that they can be manipulated
5) Operators, such as Add(+) and Multiply(*), combine Streams into new Streams
6) Operators are maximally overloaded to always work with all types of Streams
7) Programs can be labeled by other Programs, creating Pairs
8) Labeled Programs can be merged/replaced with other (labeled) Programs
9) Programs are optimally and lazily evaluated on demand (re-using computations)

Next to that, an algebra of Streams is defined, together with an algebra of Labels.
SPREAD is mono-typed with Programs. It is an ultimate attempt to create a 'better' Excel.

I have been working on a logic programming language
that I have published here [1].
In my opinion, it has a potential expressive power
superior to that of other logic languages I have studied [2],
it can reason efficiently (polynomial time),
and it is mathematically very simple (first order theory with a finite model).

I guess I must be wrong, but where am I wrong?

1.- http://pypi.python.org/pypi/Terms/
2.- prolog, CLIPS (+ COOL), the semantic web OWLs, and various offshots of those

Relations are an important vehicle to write specifications. In this article
we study some properties of binary relations. First we start from binary
relations in general with domain, range, composition, images etc.

In the second part we study endorelations i.e. binary relations where the type
of the domain and the range are the same. The most important endorelations are
transitive relations. Transitive relations have a close connection to closure
systems.

...

Christopher Hancock's dissertation, mentioned before but I think it deserves its own post somewhere, especially since it is very similar to Bret Victor's work (but is from 2003!).

Though notoriously difficult, real-time programming offers children a rich new set of applications, and the opportunity to engage bodily knowledge and experience more centrally in intellectual enterprises. Moreover, the seemingly specialized problems of real-time programming can be seen as keys to longstanding difficulties of programming in general.

I report on a critical design inquiry into the nature and potential of real-time programming by children. A cyclical process of design, prototyping and testing of computational environments has led to two design innovations:

• a language in which declarative and procedural descriptions of computation are given equal status, and can subsume each other to arbitrary levels of nesting.
• a "live text" environment, in which real-time display of, and intervention in, program execution are accomplished within the program text itself.

Based on children's use of these tools, as well as comparative evidence from other media and domains, I argue that the coordination of discrete and continuous process should be considered a central Big Idea in programming and beyond. In addition, I offer the theoretical notion of the "steady frame" as a way to clarify the user interface requirements of real-time programming, and also to understand the role of programming in learning to construct dynamic models, theories, and representations. Implications for the role of programming in education and for the future of computational literacy are discussed.

Strongly-Typed Language Support for Internet-Scale Information Sources

Don Syme, Keith Battocchi, Kenji Takeda(1), Donna Malayeri, Jomo Fisher, Jack Hu, Tao Liu, Brian McNamara, Daniel Quirk, Matteo Taveggia, Wonseok Chae, Uladzimir Matsveyeu(2), Tomas Petricek(3)

1 Microsoft Research, Cambridge, United Kingdom
2 Microsoft Corporation, Redmond WA, USA
3 University of Cambridge, United Kingdom

Abstract:

...Most modern applications incorporate one or more external information sources as integral components. Providing strongly typed access to these sources is a key consideration for strongly-typed programming languages, to insure low impedance mismatch in information access...

In this report we describe the design and implementation of the type provider mechanism in F# 3.0 and its applications to typed programming with web ontologies, web-services, systems management information, database mappings, data markets, content management systems, economic data and hosted scripting. Type soundness becomes relative to the soundness of the type providers and the schema change in information sources, but the role of types in information-rich programming tasks is massively expanded, especially through tooling that benefits from rich types in explorative programming.

What do you think of this approach?