News for hackers. Stuff that matters.

A comment on Ask HN: Is it possible to perform compile-time checks for all invariants?.

Re:Ask HN: Is it possible to perform compile-time checks for... by Davidbrcz on Monday February 17, 2025 @08:13AM (#43078640)
You can look into theorem proover (Coq, lean ...) and code extracted from them. A middle ground is FramaC+WP plugin for hoare logic for C.

Some languages like F* are also proof oriented.

[ Parent | on HN ]

There are no comments on this comment yet.