3 ms·
Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase? Maybe specifying some conditions/assertions in comm
by 0xpgm 3y ago
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.
- ianandrich 3y agoPython'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.
- 0xpgm 3y agoThank you! This is great, sounds like what I'm looking for.
- logicchains 3y ago>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.