Hacker News new | ask | show | jobs
by shadowfox 1185 days ago
What are some entry points for (say) a motivated programmer to the topic of formal verification?
2 comments
nwah1 1185 days ago
You 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

link
jonjacky 1185 days ago
Alloy, 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

Linked at the top of that page is a book about Alloy. There is also a book about TLA, mentioned in another comment here.

link