7 ms·
What are some entry points for (say) a motivated programmer to the topic of formal verification?
by shadowfox 4y ago
What are some entry points for (say) a motivated programmer to the topic of formal verification?
- nwah1 4y agoYou are on your own mostly. That's part of the problem. I am right there with you in my lack of understood in how best to get started. The most trendy language on HN (Rust) has an initiative called Prusti, and a working group. Most of the languages that are used for actual formal verification in industry settings are arcane. Like AdaSPARK. And then there a lot of academic-focused languages meant mainly to experiment with dependent types or prove math theorems. TLA+ also has some ability to support it, but not out of the box. DynamoDB at AWS was built with it. The homepage for it has some approachable resources, but for the language itself. The formal verification systems are separate. https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html
- jonjacky 4y agoAlloy, mostly used for modeling and analysis but see the program verification section about halfway down this very long page: https://alloytools.org/citations/case-studies.html https://alloytools.org/citations/case-studies.html Linked at the top of that page is a book about Alloy. There is also a book about TLA, mentioned in another comment here.