3 ms·
It was my understanding that when formal methods were used, they were used on very small subsets of code and not used in general. I do wonder about TLA+ and wou
by gregors 6y ago
It was my understanding that when formal methods were used, they were used on very small subsets of code and not used in general. I do wonder about TLA+ and would love to hear more about how they use such tools.
I know I've seen an older document that specifically prohibited use of malloc that the risk was too great. Is that still the case?
- mhh__ 6y agoFormal methods are indeed hard. They generally thrive on hardware, software is a wholly different kettle of fish in terms of the size of the problem (the actual methods are often similar, but hardware design generally encourages certain patterns that are easier to analyse) I'm not related to this project or aerospace, so I can't divine more knowledge than anyone else, although I have seen many coding standards that forbid malloc after some critical time (e.g. no dynamic memory allocation after the plane is off the ground)