Conclusion
- Alfa is more than adequate for this example
- Haskell+Plogic is less appropriate for this kind of modelling
(don't need partial functions or infinite data strutures)
- Possible future work:
- Include
runProtected
and algorithms that can fail
- Abstact away from the concrete state monad and make use of explicitly
stated monad properties instead.
- Use the Alfa certificate server and do the proof for the Haskell program
- Feasibility check: create a concrete instance with good algorithms
& associated proofs