News for hackers. Stuff that matters.

A comment on We're building a browser when it's supposed to be impossible. Parent comment

Re:We're building a browser when it's supposed to be impossible by jeroenhd on Tuesday April 11, 2023 @01:29PM (#35528309)
There are some languages that can be formally verified, and have themselves been formally verified.

Formal verification is a complete pain in the ass to do and there's a reason it's mostly done only in the most critical of systems, but if a program passes 100% formal validation, you're as close to crash free as you can possibly be.

I believe Ada and some other lesser used language sport well supported formal verification methods. You won't be able to use C/C++/Java/Rust it you're going for 100% formal verification though. There are attempts to bring the concepts to more commonly used languages (Frama-C, for example) but in my experience they're stuck in PhD-ware hell, great for writing papers but terrible for writing actual software.

[ Parent | on HN ]
Re:We're building a browser when it's supposed to be impossible by KsassPeuk on Wednesday April 19, 2023 @11:40AM (#35629574)
Frama-C is used in production to meet normative requirements for critical software at least at Airbus (DO-178C), THALES (CC EAL6/7), EDF (ISO 60880). I think that they use actual software in production.
[ Parent | on HN ]