Hacker News new | ask | show | jobs
by 0xpgm 974 days 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.
2 comments
logicchains 974 days 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.

link
ianandrich 974 days ago
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.

link
0xpgm 974 days ago
Thank you! This is great, sounds like what I'm looking for.
link