While Web development is undoubtedly easier than, say, assembly language programming, the practice is still plagued by its own specific hurdles of difficulty. One of those is the fact that Web applications often combine CSS, XML, JavaScript and HTML. But a professor at MIT is hoping to make it easier to untangle the interactions between these elements with a new form of his programming language: Ur.
Adam Chlipala, the Douglas Ross Career Development Professor of Software Technology at MIT, will present a paper at the Association for Computing Machinery on the Ur/Web version of his Web application-development language. The language is coupled with a compiler that outputs actual Web code, sans conflicts, overlaps, and the gray areas that can emerge among CSS, XML, HTML and JavaScript.
Chlipala is most commonly associated with proofs. At MIT, he teaches a course on certified programming, but he uses (in his own words) “a very unusual approach, centered on replacing manual proofs with lots of dependent types and mostly automated proofs based on scripted decision procedures.”
This makes more sense upon learning that Chlipala’s favorite development projects are functional programming languages, with a focus on expressive type systems using dependencies. His ultimate goal as a professor is to give his students the knowledge and tools (like Coq) they need to reduce the human cost of program verification.
Chlipala also likes to focus on very high or very low-level languages. Thus, his language Ur is based on dependent types. He compares the language to Haskell and ML, with the inclusion of significantly rich type systems.
Ur/Web is, essentially, Chlipala’s take on Ruby on Rails, or Python and Django: it’s a language coupled with a Web-focused library, and a compiler that turns Ur code into HTML, CSS, JavaScript and CML.
As this is a language written by a professor at MIT who’s greatly concerned with certifying programs as provably safe, correct and bug-free, Ur/Web has a few advantages over existing development models.
According to Chlipala, “Not only do [Ur programs] not crash during particular page generations, but they also may not suffer from any kinds of code-injection attacks, return invalid HTML, or contain dead intra-application links, have mismatches between HTML forms, and [have] the fields expected by their handlers.”
Chlipala also states that Ur/Web programs will never “include client-side code that makes incorrect assumptions about the AJAX-style services that the remote Web server provides; attempt invalid SQL queries; or use improper marshaling or unmarshaling in communication with SQL databases, or between browsers and Web servers.”
Ur/Web saw a new release on January 3, and is available for free.