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.