The Ur Programming Language

I worked with in the same lab as the author adam chipala two summers ago. He's a brilliant hacker/computer scientist, and any work he does is worth taking seriously.

To quote from the manual: The signature (ed: the type or interface) of the standard library is such that well-typed Ur/Web programs “don’t go wrong” in a very broad sense. Not only do they not crash during particular page generations, but they also may not:

• Suffer from any kinds of code-injection attacks

• Return invalid HTML

• Contain dead intra-application links

• Have mismatches between HTML forms and the fields expected by their handlers

• Include client-side code that makes incorrect assumptions about the “AJAX”-style services that the remote web server provides

• Attempt invalid SQL queries

• Use improper marshaling or unmarshaling in communication with SQL databases or between browsers and web servers

Thats pretty cool, and it looks like the language is able to statically catch that all using the type system (the types are presumably mostly inferred by the compiler), and presumably the error messages do or will provide informative information about the location of errors.

It is also worth noting that when you compile an Ur/web program, the executable you get is a web server dedicated to serving the page that is described by the programmer! So presumably, aside from setting up the compiler toolchain, the actual server setup is easy!

Kudos! -Carter

edit: http://adam.chlipala.net/papers/UrPLDI10/ is the link to the paper the focuses on the research novelty elements of the system.

edit2: also you got to love that the theres a formal semantics for the language and the types which makes it clear to those with the right background that theres a formal proof that the type system also prevents bad stuff from happening! :)

While it would be nice to imagine something like this catching on, somehow I suspect that any language whose reference manual gives a specification of semantics using sequent calculus before discussing the standard libraries is unlikely to gain much use.

Fast, expressive, flexible, with static analysis that can prevent entire classes of common bugs? That sounds great! Oh wait, no, it uses words that sound like math, obviously that makes it unsuitable for the real world. Sigh.

Compare: http://impredicative.com/ur/demo/Demo/Form/handler?B=there&#...

http://impredicative.com/ur/demo/Demo/Form/handler?B=there&#...

http://impredicative.com/ur/demo/Demo/Form/handler?B=there&#...

I get the first 2, but what's up with the 3rd one?

I'm trying to run the demo, and it keeps starting up emacs in order to compile html templates. It doesn't use -nw or -q, so for each file, it creates a window, loads my init files, runs a tiny bit of elisp to expand a template (or something), writes it out, and closes down emacs (running everything in kill-emacs-hook).

I could just move my emacs directory temporarily or add some reasonable commands to the process (even use emacsclient!), but I'd rather complain about it here.

I'm going to design a language called Original. The Original programming language.

Does this use lazy or eager evaluation?