[thih9]

> how different Coq users use Coq differently and express different needs

> applying Coq to do software verification

> encourage others to learn and use Coq

To be clear, some people giggle when they read or hear the above and this is the reason.