Hacker News Reader

SPARK is a real-world system that allows some degree of formal proofs in the programming language and related tools:

https://learn.adacore.com/courses/intro-to-spark/index.html

https://docs.adacore.com/spark2014-docs/html/lrm/introductio...

I've tried SPARK. Compared to Frama-C, SPARK is not as powerful. Frama-C can prove the correctness of arbitrary heap manipulation algorithms. SPARK can handle singly linked lists but not doubly linked lists (last I checked).

Although, usually the people who use SPARK use it because it is certified for their industry (such as aerospace).

Reply on news.ycombinator.com