Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
A predicate transformer semantics for effects (functional pearl)
Swierstra W., Baanen T. Proceedings of the ACM on Programming Languages3 (ICFP):1-26,2019.Type:Article
Date Reviewed: Jan 20 2021

Proving properties of imperative programs with side effects is quite arduous. Purely functional code, on the other hand, has a relatively pleasant equational theory that enables reasonable proofs. Is it possible to use modern machinery to make proofs about effectful programs easier?

The work here illustrates such a path forward. As befits the pearl style, it walks the reader slowly and steadily through the ideas, with plenty of illustrative examples along the way. Complex ideas--the “predicate transformer semantics for effects” of the title, as well as a similar semantics for specifications and a way to mix them--are made quite clear. For the expert, various concepts from category theory that underlie the semantics are sprinkled throughout.

The ideas are made clear by explicitly showing Agda code (a dependently typed programming language in the Haskell family), along with explanations of each new idea. Full code can also be found online.

As system programming languages (such as Rust) give us more features for ensuring safety, we also need to keep looking ahead to the next level of features. Anyone who wants a clear preview of the bright future such investigations have should read this paper.

Reviewer:  Jacques Carette Review #: CR147164 (2105-0115)
Bookmark and Share
  Featured Reviewer  
 
General (D.2.0 )
 
 
General (D.3.0 )
 
 
General (F.0 )
 
Would you recommend this review?
yes
no
Other reviews under "General": Date
Development of distributed software
Shatz S. (ed), Macmillan Publishing Co., Inc., Indianapolis, IN, 1993. Type: Book (9780024096111)
Aug 1 1994
Fundamentals of software engineering
Ghezzi C., Jazayeri M., Mandrioli D., Prentice-Hall, Inc., Upper Saddle River, NJ, 1991. Type: Book (013820432)
Jul 1 1992
Software engineering
Sodhi J., TAB Books, Blue Ridge Summit, PA, 1991. Type: Book (9780830633425)
Feb 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy