It's not just about whether it is possible in theory though. I'm sure it is, but if it's too complicated, it won't see adoption. The point I was making is that expressibility isn't just important in your programming language, it's important for your verification scheme as well.