Increasing confidence in dependently typed programs

There exist numerous methods for testing and verifying software, including property based testing, automatic code generation, model checking, and proof assistants. Although these tools help ensure that software behaves according to its specification, they are typically deployed in isolation rather than as reinforcements for one another. As software complexity grows, so does the complexity of modelling and checking the system. While rigorous approaches such as model checking and formal proofs provide strong correctness guarantees, these have difficulty scaling and often require reimplementing the code in a separate verification language. This risks the semantics being lost in translation, as there is no guarantee that the verified model behaves the same as the deployed code. Programming languages with dependent types – such as Idris2 ­– present novel ways to enforce correctness through dependently typed terms. However, the complexity of the dependent types also grows with the complexity of the system. This raises the question: "How does one know that the typed model used for checking matches the specification?" Since dependent types are effectively type-level programs, how might one try to ensure that they accurately model the problem and do not themselves contain errors? This thesis explores several approaches to this problem. It presents a tool for generating types and code from diagrams, leveraging human strengths in visual reasoning. Additionally, a type-level property based testing framework is presented, allowing dependently typed stateful models to be tested. Both approaches are evaluated over stateful systems of increasing complexity, with even small systems giving rise to subtle bugs in a dependently typed model. These results demonstrate the value of the tools presented, which combine multiple degrees of verification into a single system and reduce the expertise required to increase the confidence in dependently typed programs while strengthening the relation between the checked model and the implementation.