A toy PL for writing proofs inline with imperative code.
The python/ dir contains some initial ideas on syntax. The haskell/ dir contains the most recent work of proof rewriting.
If the project progresses to a semi-stable feature set and syntax, the next step will be to look into replacing/integrating the proofing system with one of Lean, Prolog, etc. Such an integration might yield benifits in correctness and/or autodeduction.