News for hackers. Stuff that matters.

A comment on Formal methods: Just good engineering practice?. Parent comment

Re:Formal methods: Just good engineering practice? by IshKebab on Monday June 24, 2024 @02:59AM (#40773183)
I don't know if that's always the case. My understanding is that TLA+ is really designed to prove properties about algorithms. Knowing that complex algorithms are correct is very useful eventually if it doesn't provide a correct implementation in a real world language.

But TLA+ is a bit of an unusual proof language. I think most of them are like you describe: SPARK, Dafny, F*, CBMC, all the Rust ones, etc. I'm not sure about the interactive proof languages (Coq et al), they are too complicated for my normal sized brain.

[ Parent | on HN ]
Re:Formal methods: Just good engineering practice? by pjmlp on Monday June 24, 2024 @05:21AM (#40773950)
Yes, and making those languages (SPARK, Dafny, F*, CBMC,....) more widespread, the kind of something that everyone expects to be out of the box on their favourite language is how this can eventually gain more adoption, than a few selected companies, or academic research.
[ Parent | on HN ]