Program analysis has witnessed two dominant trends in recent years. On one hand, declarative languages such as Datalog and its variants are increasingly used to specify sophisticated program analyses. On the other hand lies the advent of Big Code which seeks to leverage large repositories of source code, test cases, and meta-information to predict program properties. I will describe challenges and opportunities at the intersection of these two trends, towards the goal of developing effective program reasoning tools for deployment in large software projects and interaction with software engineering practices.