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.
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.