News for hackers. Stuff that matters.

A comment on F’: Flight Software and Embedded Systems Framework. Parent comment

Re:F’: Flight Software and Embedded Systems Framework by pensono on Friday February 19, 2021 @08:51PM (#26200667)
Is C++ complex enough that it is difficult to model, and therefore hard to apply in formal methods?
[ Parent | on HN ]
Re:F’: Flight Software and Embedded Systems Framework by rurban on Saturday February 20, 2021 @12:04AM (#26201746)
The problem is not the language, the problem are unbounded loops. Like linked lists vs vectors. Termination is theoretically impossible to prove, but practically you can handle it.

Parts of the STL were formally verified. cprover (with satabs and cbmc) can handle C, C++ or Java. F' uses autogenerated classes, which helps a lot avoiding mistakes.

[ Parent | on HN ]
Re:F’: Flight Software and Embedded Systems Framework by gugagore on Saturday February 20, 2021 @10:02AM (#26204560)
Because the problem is unsolvable, there is a wide variety of "you can handle it"-ness that a language can have...
[ Parent | on HN ]