I have long wanted to add proposition types and proofs to my hobby programming language (which I talked about at the Wellington SAPLING). I think I've figured out how to do it. Obviously I should shut up till I have some running code, but I happen to be in the Sydney-Canberra area this week (actually in smokey Canberra, but happy to come to Sydney). So if anyone is interested I can talk or give a talk (I would just work through a particular example: showing that Nat with + is a semigroup). I think it could be done in a similar way in many languages.
If someone with actual experience with proving stuff about programs wants to help me find the errors in my plan before I make them, then that would be even better.
Next week I'm thinking of visiting my brother in smoke-free Queensland, and after that I'll be back in Melbourne, in case those locations suit anyone.