Certiï¬ed Web Services in Ynot
In this paper we demonstrate that it is possible to implement certiï¬ed web systems in a way not much diï¬€erent from writing Standard ML or Haskell code, including use of imperative features like pointers, ï¬les, and socket I/O. We present a web-based course gradebook application developed with Ynot, a Coq library for certiï¬ed imperative programming. We add a dialog-based I/O system to Ynot, and we extend Ynotâ€™s underlying Hoare logic with event traces to reason about I/O behavior. Expressive abstractions allow the modular certiï¬cation of both high level speciï¬cations like privacy guarantees and low level properties like memory safety and correct parsing.
Ynot, always ambitious, takes another serious swing: extracting a real web application from a proof development. In some respects the big news here is the additional coverage that Ynot now offers in terms of support for file and socket I/O, and the event trace mechanism. But there's even bigger news, IMHO, which is the subject of another paper that warrants a separate post.