Lambda the Ultimate

Lunascript, our in-house language for writing great web apps:

Inspired by incremental computing, we're building Lunascript as a simple way to write modern web applications. Lunascript has a syntax and easy of use reminiscent of JavaScript, but a powerful pure-functional lazily-evaluated semantics historically confined to academic languages.

A Lunascript application specifes a data model and a function from the model to the view or user interface, annotated with handler functions from user inputs to model mutations. From this the Lunascript compiler produces a functioning Web2.0 application -- the client-side JavaScript, the server-side SQL, and everything in between -- complete with real-time bidirectional data synchronization.

I'll have to wait for more info on this definitely interesting project, but right now I'm a bit sceptical, as this seems to throw REST out the window.

Continuity Analysis of Programs, Swarat Chaudhuri, Sumit Galwani, and Roberto Lublinerman. POPL 2010.

We present an analysis to automatically determine if a program represents a continuous function, or equivalently, if infinitesimal changes to its inputs can only cause infinitesimal changes to its outputs. The analysis can be used to verify the robustness of programs whose inputs can have small amounts of error and uncertainty -- e.g., embedded controllers processing slightly unreliable sensor data, or handheld devices using slightly stale satellite data.

Continuity is a fundamental notion in mathematics. However, it is difficult to apply continuity proofs from real analysis to functions that are coded as imperative programs, especially when they use diverse data types and features such as assignments, branches, and loops. We associate data types with metric spaces as opposed to just sets of values, and continuity of typed programs is phrased in terms of these spaces. Our analysis reduces questions about continuity to verification conditions that do not refer to infinitesimal changes and can be discharged using off-the-shelf SMT solvers. Challenges arise in proving continuity of programs with branches and loops, as a small perturbation in the value of a variable often leads to divergent control-flow that can lead to large changes in values of variables. Our proof rules identify appropriate “synchronization points” between executions and their perturbed counterparts, and establish that values of certain variables converge back to the original results in spite of temporary divergence.

We prove our analysis sound with respect to the traditional epsilon-delta definition of continuity. We demonstrate the precision of our analysis by applying it to a range of classic algorithms, including algorithms for array sorting, shortest paths in graphs, minimum spanning trees, and combinatorial optimization. A prototype implementation based on the Z3 SMT-solver is also presented.

Another fun paper from POPL this year. I've seen metric spaces used to solve domain equations before, but the idea of actually considering a metric on the outputs was a new one to me.

I am looking for any papers that analyze the design of cascading stylesheets with respect to bounded times. I could derive this myself, but it would be nice to have a peer reviewed authority. It would also be cool if anyone ever bothered to do this for Hakon Wum-Lie's original CHSS (Cascading HTML Style Sheets) and Bert Bos's original SSP (Stream-based Style Sheet Proposal) prior to them being merged into CSS 1.0. Also, Dynamic Properties that were in Internet Explorer from 5.0 through 7.0, but deprecated in 8.0.

The only thing I found so far was a webpage: CSS, selectors and computational complexity. However, this doesn't communicate the complexity on how selectors place solving constraints on the layout engine to update each widget's CSS box model.

I'm also interested in knowing if anybody has done anything to model compatibilities across browsers. All I found was this (mindblowing) Comparison of layout engines and their support for CSS.

I don't think anyone has actually done anything to formally investigate the most widely used DSL in the world and the affect it has on clockcycles as well as programmer man-hours...

Thanks.

I've just begun reading Whitehead and Russell's "Principia Mathematica" available here and was surprised to find on page 9 a nice readable alternative to parentheses for grouping.

Each operator is preceded and/or succeeded by some dots written as colons and periods. The more dots an operator has, the lower precedence it has. To take one of their examples (page 10),
p -> q .->. q -> r :->. p -> r
means
((p -> q) -> (q -> r)) -> (p -> r)

I find the dot version more readable and easier to type than the parentheses version. I'm curious if anyone here knows of other alternatives to parentheses for grouping. Prefix and postfix we've all heard of here, but do you have less well known ones? Hideous or beautiful I'd love to see them! Have any been tried in programming languages?

Prompted by Z-bo's question of what is there to gripe about CSS, I thought I'd point out the Clutter toolkit:

Clutter is an open source software library for creating fast, visually rich, portable and animated graphical user interfaces.

Clutter uses OpenGL (and optionally OpenGL|ES for use on Mobile and embedded platforms) for rendering but with an API which hides the underlying GL complexity from the developer. The Clutter API is intended to be easy to use, efficient and flexible.

Similar to Bling, it explores how GPU abstractions should be exposed to UI layout designers. I think there will be a lot of turmoil in this space over the next few years. Some related projects of interest are PixelBlender (with its integration into Flex 4) and similar projects in the Silverlight community. Another approach is to try to not change anything, as in a new GPU-accelerated Firefox branch. The only comparable approach I know of in the PL space is Conal Elliott's Vertigo, but that was not really about structured UI.

Edit: link fixed.

Edit 2: two big motivations here 1) performance on mobile devices and 2) enabling new types of UIs, such as physically realistic ones