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.