HasCal — A promising embedding of pluscal in haskell.

art yerkes
2 min readApr 17, 2022


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
data Global = Global
{ _number :: Int
, _output :: Int
} deriving (Eq, Generic, Hashable, Show)
instance Pretty Global where pretty = unsafeViaShowmakeLenses ‘’GlobaltestNatDivision :: IO ()
testNatDivision = do
let startingLabel = ()
let startingLocals = pure ()
let nd2 = do
while (do v <- use (global.number) ; return (v >= 2)) do
global.output += 1
global.number -= 2
let process = do
initial_n <- use (global.number)
initial_o <- use (global.output)
global.output -= initial_o
nd2 my_output <- use (global.output)
assert (initial_n `div` 2 == my_output)
model defaultOptions { debug = True } Begin {..} (pure True) do
_number <- [ 1 .. 1000 ]
_output <- [ 0 ]
return Global {..}
main :: IO ()
main = do

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.



art yerkes

An old programmer learning new tricks.