# 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+:

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.

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 HasCaldata 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

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.