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
data Global = Global
  { _number :: Int
  , _output :: Int
  } deriving (Eq, Generic, Hashable, Show)
instance Pretty Global where pretty = unsafeViaShow
makeLenses ‘’Global
testNatDivision :: 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
  testNatDivision

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.