HasCal — A promising embedding of pluscal in haskell.

I’ve been interested in proof systems and proofs for a while. Recently, I took my first tiny step (a very bad example) in TLA+:

A very bad example of a simple Nat div2 check in TLA+

I’ve been following Gabriella Gonzalez’ HasCal for a while, and decided to spend a short time trying it out. It’s a bit weird (and has some weaknesses and blindspots for now) but works pretty well and may be more tractable for those who know haskell but not TLA+. What’s there is really promising.

A neat embedding of PlusCal in haskell

The whole thing is based on a monad that allows a fairly concise representation of TLA+ code in do notation. I did a quick port of the code above based on the euclid’s algorithm test example and it’s even a bit more general than my attempt at TLA+ (admittedly I don’t know the pattern for testing just a function). I don’t claim to be any kind of expert in TLA+ but I think I’ll try it a bit more in the form of HasCal as it’s very familiar syntactically. I wonder how hard it’d be to port to idris and mix with dependent types :-)

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
import Control.Monad (when)
import HasCal

Using this method you can basically emulate any kind of computation and TLA+ allows checking of ongoing process invariants via coroutine and property members of the model. Happily, it’s very easy to get started and try it out.

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store