LtU Forum

Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU)

We are having another PLATEAU workshop at SPLASH 2014. We have a new category for "Hypotheses Papers" and thought this would be particularly appealing to the LTU community.

http://2014.splashcon.org/track/plateau2014

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.

PLATEAU gathers the intersection of researchers in the programming language, programming tool, and human-computer interaction communities to share their research and discuss the future of evaluation and usability of programming languages and tools.

Some particular areas of interest are:
- empirical studies of programming languages
- methodologies and philosophies behind language and tool evaluation
- software design metrics and their relations to the underlying language
- user studies of language features and software engineering tools
- visual techniques for understanding programming languages
- critical comparisons of programming paradigms
- tools to support evaluating programming languages
- psychology of programming

Submission Details

PLATEAU encourages submissions of three types of papers:

Research and position papers: We encourage papers that describe work-in-progress or recently completed work based on the themes and goals of the workshop or related topics, report on experiences gained, question accepted wisdom, raise challenging open problems, or propose speculative new approaches. We will accept two types of papers: research papers up to 8 pages in length; and position papers up to 2 pages in length.

Hypotheses papers: Hypotheses papers explicitly identify beliefs of the research community or software industry about how a programming language, programming language feature, or programming language tool affects programming practice. Hypotheses can be collected from mailing lists, blog posts, paper introductions, developer forums, or interviews. Papers should clearly document the source(s) of each hypothesis and discuss the importance, use, and relevance of the hypotheses on research or practice. Papers may also, but are not required to, review evidence for or against the hypotheses identified. Hypotheses papers can be up to 4 pages in length.

Papers will be published in the ACM Digital Library at the authors’ discretion.

Important Dates

Workshop paper submission due - 1 August, 2014
Notification to authors - 22 August, 2014
Early registration deadline - 19 September, 2014

Keynote

Josh Bloch, former Chief Java Architect at Google and Distinguished Engineer at Sun Microsystems.

Do Logic Languages Need Negation?

I have been working on an interpreter for a mini-subset of Prolog as I find it interesting how logic languages hold a central place in proof-assistants, theorem-provers and type-systems.

What I am interested in is a minimal and sound dialect of prolog to server as a starting point for further investigation. There are obviously several design points to discuss, but negation appears to be the most fundamental. Obviously as I am interested in soundness I want to operate in a Herbrand universe, which means unification with an occurs check.

The problem with negation seems to stem from the Prolog programming model. It appears to me that at some point "failure/unsat" and "falseness" (and "success/sat" and "truthfulness") have become confused with each other. This leads to negation as failure, the unsoundness of which is easily shown:

:- not (not (X = 0)), not (not (X = 1)).
yes.

Various solutions to this have been proposed, three-valued (Kleene) logic, four valued (Belnap) logic, negation as inconsistency, negation as refutation etc. All of those complicate the resolution process, but do solve the problem. Strong negation seems interesting because it is local and not fragile like some of these methods. I particularly liked the combination of a four-valued logic (because the bilattice structure is nice) and strong negation, and started to look at implementing it.

What interested me is that the logic values are seen as success values, so that a functor can be 'true' or 'false' without failing. In which case, why make them special 'values' in the language at all, surely they can be treated as normal atoms? Taking list membership as an example, we might want to define:

member(Key, cons(def(Key, _), _), true).
member(Key, nil, false).
member(Key, cons(_, Tail), X) :- member(Key, Tail, X).

We can even define 'not' as a predicate (fail if arg is true):

not(false).

not_member(Key, List) :- member(Key, List, X), not(X).

or a binary operator

not(true, false).
not(false, true).

not_member(Key, List, X) :- member(Key, List, Y), not(Y, X).

Without any of the logical unsoundness of negation as failure. There is obviously a parallel with dependent type systems (curry-howard), which I don't think have negation.

I have put the source code for my simple logic language "Clors" on GitHub https://github.com/keean/Clors. Its a still experimental, and is suffering form many changes and false starts, so needs a little tidying up (I have just removed meta-interpreters because they turn out to be unsound), and needs updating to use my parser combinator library.

So the question is, do logic languages need builtin negation?

'Mindless coding': following proof steps makes algorithms easy

Mindless Coding, uses Coq to emit Ocaml:

Fully-specified dependently typed structures (avltree and rbtree) and their functions (find, insert, delmin and delete) not only produce fully verified results - they also reduce the task of function implementation to a stepwise refinement of intermediate steps (proof subgoals) that are constrained to the point where the programmer (prover) is freed from consideration of the overall algorithm involved during each step. In many cases, the steps are fully automatable. In others, the information provided by the subgoal's context, along with a "rough idea" of what the algorithm being implemented should do, is usually sufficient for the programmer to make progress to the next subgoal.

Perhaps the best illustration of this "mindless" point is the implementation of the complex rebalancing functions for Red-Black trees, which are widely viewed as difficult to do correctly. These were implemented using this "mindless-coding" technique without relying on any outside explanatory material or implementations.

'Mindless' if you are smart enough to be able to do incremental steps in proof-making :-)

Dynamic Hindley-Milner?

Does anyone know of any work where HM-style type inference is performed at run-time rather than compile time? By this, I mean unification with type variables dynamically using precise (run-time) types.

request for namespace binding service terminology

(This is about semantics in a programming language for creation of responders.) I've been thinking about something off and on recently, and I wonder what the name of this idea is within the context of PL (programming language) terminology, if there is a standard name. If there's not a conventional name, I wonder if it resembles anything else. Also, if the idea itself seems incoherent, or inferior to a better way of looking at it, I'd like to hear that too.

When we write code to pragmatically do something, it calls an interface that already exists, that is already established, which is ready to respond to such invocation. At a given moment in time, some number of callable functions exist in a current process, as well as executable programs in an operating system context, and reachable servers over comm systems (of which networking is a subset). Tools at hand willing to respond to new uses thus offer affordances for latent services that can be invoked. System design includes arranging affordances you need for an app will exist at runtime, and bringing up a complex system — when it starts — typically involves carefully ordered initialization so components are ready before actual first use, or can lazily wait until a service is ready.

The idea I'm thinking of is related to boot-strapping, but that idea often refers to traversing a well-known path known statically ahead of time: getting from start at A to everything ready to go at B, where A and B are pretty much the same most of the time. I'm interested in how one plans a programming language or app framework (etc) so the concept is explicitly addressed by the tools, so there's a way to talk about designing points A and B in time, within a programming language for example. It's related to both compile-time build processes as well as runtime data structure creation necessary when a program starts before some operations can be supported. If servers and other actors are launched and wait to handle messages and connections, it's also about language used to describe timing, types, and semantics of such behavior.

If you write an app with a virtual file system, a configuration phase that mounts resources where they can be found by clients later is also under the same semantic umbrella. Managing namespaces in general, and actually creating bindings at runtime are also semantically related. So module systems in a programming language touch part the same topic, if the element of time is explicitly handled. Managing dynamic evolution of binding systems in time is the part I want a sub-lexicon of terminology to address, rather than devs merely assuming an implicit common understanding no one ever talks about. (It's hard to bring language tools to bear on things never encoded.)

I know Erlang has conventions for managing restart of processes that fail, and that sort of thing. Is there a larger practice outside Erlang that gives names to elements of service management? Best would be terminology that is applicable at all times during programming execution, and not just launch, so it's easy to talk about stopping and restarting embedded sub-systems without terminating host operating system processes, with jargon re-usable outside just one framework. Every time you think of another word that gets used to describe part of such processes, I might find it useful, so even short posts mentioning specific words is helpful.

My point in posting here? It seems reasonable for a programming language to be able to write specifications for time dependent behavior of bindings visible when starting and stopping visibility of callable entities with dependencies on one another. I suppose I could re-purpose terminology used for a narrow context for use in a more general way, but that easily confuses people.

Synth Specification Overview

As I promissed to natecull, here is a 7 pages Synth specification overview: document

It explains its basic state machine functionality and brings a neat integration of reactive programming. All critics are welcome, as it is still at development stage and it can be changed until its release time.

The Programming Languages Enthusiast

http://www.pl-enthusiast.net/.

Very niche, though; just a narrow focus on a few PL topics.

Gradual Instantiation

Is anyone familiar with a language that allows for "gradual instantiation". What I mean by this, is that the initial algorithm can be stated using very vague types (but not no type) that are gradually narrowed until they reach machine language level. For example, Number -> Rational -> Float -> IEEE_754. or CustomerData -> ShippingCustomer -> AmazonCustomer -> {name, address, [items]} -> { String, {String,String,String, Number}, [String] } ... and so on. A language that supports this would need a monotonically reducing type system with some way of checking types at each level and detecting conflicts. For example: Number = Number + Number is fine, but Rational = Number + Number, requires that the RHS needs to be Rational as well (but no resolution specification, yet).

Covariance issue when extending "enter" part in BETA?

I spent bit of time recently reading up on BETA and gbeta, and I've run into a question that I haven't seen answered. I'm not sure if this is appropriate to LtU, but I honestly can't think of many other places where I could ask this and expect a meaningful/accurate response.

In BETA, when I extend or further-bind a pattern, I can add new part object declarations, as well as add to the "enter," "exit," and "do" parts. The thing is, wouldn't adding to the "enter" part mess with subtyping/covariance? Cast in more common OOP terminolgy, this would be like allowing a programmer to override an inherited virtual method and add additional parameters!

Do BETA/gbeta make this a run-time error? Do they just leave variables uninitialized in cases where not enough values are provided as input to a pattern? I haven't seen any statements on this point.

In Spark I had to put a bit of thought/effort into resolving this issue, so I wouldn't be surprised if there were prior work I just wasn't aware of.

Is Rx FRP?

There is some talk on Hackernews (see also this) that functional reactive programming should be defined as programming that is reactive and functional. Such "FRP" would then include event streaming dataflow programming systems like Rx. Is the dilution in terminology worth it and I'm just being pedantic, or is there some genuine confusion in hacker land?

XML feed