New Language from MIT Streamlines Building SQL-Backed Web Applications
There are countless developers and administrators who are creating and deploying online applications backed by SQL databases.
That's exactly the problem that Adam Chlipala, an Assistant Professor of Electrical Engineering and Computer Science at MIT, is trying to solve with Ur/Web, a domain-specific functional programming language for modern Web applications. The language encapsulates many key components needed for robust applications into just one language, and can help ensure the security of the applications.
"My research applies formal logic to improve the software development process. I spend a lot of time proving programs correct with the Coq computer proof assistant, with a focus on reducing the human cost of program verification so that we can imagine that it could one day become a standard part of software development (at least for systems software). I'm also interested in the design and implementation of programming languages, especially functional or otherwise declarative languages, especially when expressive type systems (particularly dependent type systems) are involved. I usually stick to very low-level or very high-level languages; I believe that most 'general-purpose languages' of today fail to hit the mark by being, for any particular software project, either too low-level or too high-level."
Chlipala also emphasizes that Ur/Web is not only a research prototype. It has a growing programmer community and some commercial application development underway. As an explanatory page notes:
"Ur/Web supports construction of dynamic web applications backed by SQL databases. The signature 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
- - Attempt invalid SQL queries
- - Use improper marshaling or unmarshaling in communication with SQL databases or between browsers and web servers
"This type safety is just the foundation of the Ur/Web methodology. It is also possible to use metaprogramming to build significant application pieces by analysis of type structure. For instance, the demo includes an ML-style functor for building an admin interface for an arbitrary SQL table. The type system guarantees that the admin interface sub-application that comes out will always be free of the above-listed bugs, no matter which well-typed table description is given as input."
"The implementation of all this is open source."
You can get the latest distribution of Ur/Web here.