The concrete examples the author is looking for, where it's easier to analyze programs according to their behavior instead of their imperative structure, is Per

The concrete examples the author is looking for, where it's easier to analyze programs according to their behavior instead of their imperative structure, is Per Martin-Löf's paper Constructive Mathematics and Computer Programming (DOI: 10.1016/S0049-237X(09)70189-2). For a brief and intuitive explanation, see this post by Robert Harper on the RedPRL prototype that uses cubical computational type theory https://existentialtype.wordpress.com/2018/01/15/popl-2018-tutorial/ https://existentialtype.wordpress.com/2018/01/15/popl-2018-t... You can also have your legacy cake and eat it too with this excellent recent paper on gradual typing https://arxiv.org/pdf/1802.00061v2.pdf https://arxiv.org/pdf/1802.00061v2.pdf "This allows for the introduction of new typing features to legacy languages and codebases without the enormous manual effort currently necessary to migrate code from a dynamically typed language to a fully statically typed language. Gradual typing allows exploratory programming and prototyping to be done in a forgiving, dynamically typed style, while later that code can be typed to ease readability and refactoring."