4 ms·
I love math and a good type system. I know little about formal verification of code. Are there tools (ideally) or languages (for educational, if not production,
by HWR_14 4y ago
I love math and a good type system. I know little about formal verification of code. Are there tools (ideally) or languages (for educational, if not production, use) you recommend I look at?
- mrslave 4y agoI went through Benjamin Pierce et. al - Logical Foundations [0] which uses Coq. It was great fun, and I am someone who has a pattern of shying away from mathematics a little too often. That said, I'm not the right person to tell you why and when Coq > all other proof systems. Pierce is famous though, and so are his books. [0] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/