This talk is an overview of the domain of neural network verification, given from the perspective of the research team implementing the domain-specific language Vehicle for specification and verification of properties of neural networks. The talk focuses on “What? ”s for major successes and “Why? ”s for major failures in this field so far; and explains the (potential) role of declarative programming in its past and future successes. Vehicle uses a range of declarative languages, including the SMT solver Marabou as a backend, Haskell as the main host compiler, and Agda as an additional backend for more complex proofs. It is designed to allow for further declarative backends, such as Coq, Imandra and KeYmaera X. The talk features a quick demo of Vehicle in its use, and reflects on its potential applications, including i) natural language processing, ii) security, iii) cyber-physical systems, as well as iv) teaching principles of neural network verification to postgraduate students.