Lambda the Ultimate

Predicate calculus is an indispensable tool for program verification. Therefore any program verifier has to be able to reason with quantified expressions, i.e. universally and existentially quantified expressions.

The proof engine of Modern Eiffel is able to perform such reasoning. The following article
"Quantified Expressions and Predicate Calculus" describes the way in which Modern Eiffel's proof engine handles quantified expressions.

The previous articles Introduction to the proof engine and Proofs by contradiction illustrate the basics of the proof engine.

PL icon Erik Meijer recently published an ACM article covering Reactive Extensions (aka Rx). As Erik notes in the article (emphasis mine) "the goal of Rx is to coordinate and orchestrate event-based and asynchronous computations such as low-latency sensor streams, Twitter and social media status updates, SMS messages, GPS coordinates, mouse moves and other UI events, Web sockets, and high-latency calls to Web services using standard object-oriented programming languages such as Java, C#, or Visual Basic."

His conclusion:

Web and mobile applications are increasingly composed of asynchronous and real-time streaming services and push notifications, a particular form of big data where the data has positive velocity. This article has shown how to expose asynchronous data streams as push-based collections of type IObservable (in contrast to pull-based collections of type IEnumerable) and how to query asynchronous data streams using the fluent API operators provided by the Rx library. This popular library is available for .NET and JavaScript (including bindings for prevalent frameworks such as jQuery and Node) and also ships in the ROM of Windows Phone. F#'s first-class events are based on Rx, and alternative implementations for other languages such as Dart7 or Haskell6 are created by the community.

What do you think of the Rx approach to asynchronous computation?

I've started a new blog in which I'm attempting to explain category theory concepts to programmers, using JavaScript as the programming language---yes, I'm using a dynamically-typed imperative language for teaching category theory. Come join the discussion at http://jscategory.wordpress.com.

Has anyone seen an objective comparison, e.g., quantitative analysis, of whether unit testing will find the bugs an ML-ish type system will reveal? There are additional benefits to both approaches, and many claims and anecdotal experiences about these things, but I'm wondering if anyone has seen anything more objective?

For example, the DiamondbackRuby etc. guys might have something like a true positive and false positive rate on checking codes that were only unit tested.

Edit: Ask and ye shall receive (in a tiny part): a study of the bugs found by translating some unit tested Python apps into Haskell.

Here* is a a paper that was accepted for publication at Onward! 2012 related to the crazy PL idea that I posted about a few months ago and a follow up of my last Onward! paper.

Abstract:

Programmers demand more extensive class libraries so they can reuse more code and write less of their own. However, these libraries are often so large that programmers get lost in deep hierarchies of classes and their members that are very broad in number. Yet language designers continue to focus on computation, leaving tools to solve library exploration problems without much help from the language.

This paper applies language design to improve IDE code completion that enables in-situ library exploration. Inference tackles depth by listing completions as long as the program can be “fixed” to support their selection; e.g. “pressed” can be listed as a widget completion since a widget can be a button. Influence mitigates breadth by leveraging types as completion selection models; e.g. a pressed event is more likely to be used on a button than a mouse event. We apply this design to YinYang, a language for programming simulations on tablets using touch-based menus.

* Hopefully skydrive behaves better than last time.

I will have to implement a complicated static code analyzer.

I have been using SOOT. It is not hard but but it seems time-consuming to get acuqinted with their large amount of API.

I believe a easier way is to use Python,
(Look at this link
http://suif.stanford.edu/~courses/cs243/hw6/hw6.html )

But I really do not want to start from "Helloworld. " Would you PL guys who happen to know Python tell me where should I start to learn Python for this usage?

Thanks.

My goal in extending an ANF-style IR has three related parts.

1. Segregate conditional tests from boolean expressions with results bound to variables (or temporaries). Conditional tests always have explicit test operators.
2. Segregate conditional branch continuations from other expressions
3. Avoid "code explosion" in expansion of short circuiting boolean test expressions.

My premise is that this extended IR is trivial to produce during normal ANF conversion and that the extended IR is more compact and easier/faster to further analyze.

The following three code snippets illustrate the "test/branch" extensions I'm exploring.

// Input source.
if a < b or big-test(a) then
  do-A(a)
else
  do-B(b)

// "Traditional" ANF-style IR 
// I hope I got the ANF rules right here.
let _t1 = a < b in
let _t2 = if not _t1 then 
            let _t3 = big-test(a) in
            if _t3 then true
            else false;
          else true
in if _t2 then
      do-A(a)
   else do-B(a)
       
// ANF-style IR extended with test/branch constructs
// %lbls are if/else branch continuations and targets for %jmp
// %ift handles some set of primitive tests in the IR
// %tr tests whether a variable warrants positive branching
%lbls _lbl1 = do-A(a);
      _lbl2 = do-B(b)
in %ift a < b then %jmp _lbl1  //  '<' is a primitive test here
   else let _t2 = big-test(a) in
        %ift %tr _t2 then %jmp _lbl1
        else %jmp _lbl2

My questions are (1) have others made similar extensions to ANF-style IR's in the past and (2) or am I just on the wrong track.

Many thanks in advance!

- Scott

I believe Dr. Shapiro posts here sometimes, and I'm sure plenty of people here have already seen and read the post, but for those of you who wouldn't otherwise see it:

Retrospective Thoughts on BitC answers: What Ever Happened To BitC?

In the large, there were four sticking points for the current design:

The compilation model.
The insufficiency of the current type system w.r.t. by-reference and reference types.
The absence of some form of inheritance.
The instance coherence problem.

Hello all!

First let me emphasize I'm a bit of a noob with language design and implementation, so feel free to dumb things down in response (in fact I would prefer it!)

I'm interested in the possibility of generating code for hard-real-time software from a declarative language. Two examples I've seen are Lustre (for reliability software) and Erlang (not sure how this could work actually since it's a general purpose language...) But when I dig down to find out exactly HOW we know that these systems generate real-time code, I come up empty handed. Where are the white papers / books / etc on how to determine a) that real-time code can be generated from a particular semantics in the first place, and b) how is the code actually generated in practice? Alternatively, how might we answer the same questions for soft-real-time code generation? Finally, can we answer this question for VMs as well, such as with .NET CIL code?

Hopefully this area of research isn't still a black art :)

In 2002, Todd Proebsting gave a talk about disruptive programming language technologies. I see that we talked about this 6 years ago and even earlier in 2002 but it seems like the right time that we talk about this again. What has been disruptive in the past 6 years and what will be disruptive in the next 10? We can talk either about technologies or the results themselves. I'll seed this topic with some initial posts.