adding Propositional types to an ordinary programming language

Skip to first unread message

Robert Smart

Jan 12, 2020, 7:09:13 PM1/12/20
Hi FPers,

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.


Robert Smart
0400 142964
Reply all
Reply to author
0 new messages