Proof Carrying Code is a long tradition within programming language research, broadly referring to methods that interleave verification with executable code, thus avoiding the inevitable discrepancies that arise when the code and the proofs are handled in different languages. Although the term was coined by Necula almost three decades ago, with time, it grew to encompass any languages that are powerful enough to handle both the coding and the proving.

An equally impressive, though very different in nature, revolution has happened elsewhere in computer science: machine learning methods grew in quality, diversity and quickly proliferated to different applications. Machine learning attracted attention of programming language researchers, and there have been recent advances in functional algorithms for automated differentiation, probabilistic programming, as well as neuro-symbolic programming and neuro-symbolic theorem proving. The latter two look into, respectively, methods of merging machine learning code and standard (symbolic) code; and automating theorem proving with the help of machine learning deployed at the stage of proof search or lemma conjecturing.

The natural question to ask is: does the concept of proof-carrying code bear any value, or indeed meaning, in the age of the neuro-symbolic paradigm shift? In this invited talk I will answer both questions in the positive. I will introduce the concept of “proof-carrying neuro-symbolic code” and explain its meaning and value, from both the “neural” and the “symbolic” perspectives. I will outline the first successes and challenges that this new area of research faces.