Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase?
Maybe specifying some conditions/assertions in comments and have it verified using some static analysis tool? Though I recognize it could be quite a challenge in dynamically typed languages.
>Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase
Running a JavaScript codebase through the Typescript compiler is a lightweight way to do incremental proof checking, albeit it can only check proofs about the soundness of the code.
Python's Deal library provides contracts and a small portable formal proofs area of the codebase.
Additionally, Deal integrates with CrossHair which does concolic execution of the tests and functions annotated with contracts. It's integrated with Z3, and most of the Python primitives are covered.
It just works surprisingly well for incrementally building up provable code properties.
Maybe specifying some conditions/assertions in comments and have it verified using some static analysis tool? Though I recognize it could be quite a challenge in dynamically typed languages.