Random notes and concluding remarks

Readability of proofs?

• I used the most compact proof representation, only the names of proof rules are visible (like a proof script in a tactical theorem prover). Being familiar with the proof rules makes it easier to understand the proof...
• Proof rules are just functions from libraries. Everything is available for browsing in Alfa.
• Natural deduction style proofs would be more self-explanatory, easy to obtain, but less practical since they would not fit on my screen.

Certificate machinery

• Certificates can not (yet) record dependencies between proofs, so there is no certificate that says
  CondSeparation, AllGoodAlgs, SameState ⊢ Separation

Random notes

• No existential quantification was used.
• Being restricted to a first-order logic is frustrating, and seems very unnatural to a functional programmer! Some general, reusable properties of state monads could not be formulated, so I had to resort to a a less modular solution. (Suggestion: extend P-Logic syntax to higher-order logic. We don't expect all proof tools to support every aspect of the logic anyway...)
• The code was not developed in accordance with "extreme formal methods" approach advocated in the Programatica project ==> Program structure and proofs more complicated than necessary.

Conjectures

• The operators inFst and inSnd, intended to provide separation by types, have a very small role in the proof. Eliminating them would simplify the model somewhat and not significantly complicate the proof.
• The proof of AllGoodAlgs depends on the memory allocation function always returning address zero, but it would be easy to change the protected memory monad to implement relative addressing, thus preserving the separation property even when packets are store at arbitrary locations in memory. This would make it possible to prove separation for a more realistic, concurrent chip model.
• There seems to be some other redundancy (unnecessary complications) in the model. It seems possible to generalize and simplify it (and hence the proofs). (The current model would just be a special case.)
• The proofs of AllGoodAlgs and CondSeparation have the same overall structure (bisimulation), so it should be possible to simplify the proofs by factoring out some reusable parts.