taylor.town about now spam rss

Publishable Network Contracts in Scrapscript

This was a last-minute abstract submission to UNSOUND 2024.

As networked programs change, the communication between sound programs inevitably becomes unsound.

Surprisingly, there exist no practical means of maintaining contracts between networked programs. Software developers suffer accordingly:

In summary, unsoundness creeps between the boundaries of the following ad-hoc systems:

Scrapscript prevents some of these errors via a holistic combination of programming lanugage features, type-system guarantees, and ecosystem defaults:

address : req => res =>
  { ip : text
  , port : int
  , unsafe-at : timestamp
  , protocol : { req, res }
  }
-- sends a record to my-address and awaits a list of ints
app-send my-address { foo = "hello" }
. my-address : address { foo : text } (list int) =
    { ip = "a31f:3dce:9990:dd92:3636:4786:9099:c665"
    , port = 81
    , unsafe-at = 1721100422
    , protocol =
      { req = t::text |> tmap (foo -> {foo})
      , res = t::list t::int
      }
    }
. t = scrap/type
. tmap = scrap/type/map