I introduce a new functional programming language, called Laconic/Web, for rapid development of web applications. Its strong static type system guarantees that entire sequences of interaction with these applications ``can't go wrong.'' Moreover, a higher-order dependent type system is used to enable statically-checked metaprogramming. In contrast to most dependently-typed programming languages, Laconic/Web can be used by programmers with no knowledge of proof theory. Instead, more expert developers develop libraries that extend the Laconic/Web type checker with type rewrite rules that have proofs of soundness. I compare Laconic/Web against Ruby on Rails, the most well-known representative of a popular class of Web application frameworks based around dynamic languages and runtime reflection, and show that my approach leads both to more concise programs and to better runtime efficiency.
Project web site