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.
