3 ms·
Most of the articles I've read about formal methods feel like lead gen for consultants. That's fine but feels obnoxious when they implicitly act as though they
by thefaux 2y ago
Most of the articles I've read about formal methods feel like lead gen for consultants. That's fine but feels obnoxious when they implicitly act as though they have reached formal methods induced enlightenment that you can too if you buy a pack of trainings for your employees/coworkers or hire me as an employee to fix your bad (irresponsibly dangerous even!) programming habits.
Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec.
- erpellan 2y agoHow about https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)
- lolinder 2y agoAda is terminally underappreciated.
- MaxBarraclough 2y agoSeconded. Regarding applying SPARK, the Tokeneer case-study is an interesting read. It's self-published by AdaCore. This summary page links to the full PDF: https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer
- aiono 2y ago> Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec That would be useful but there is a fundamental issue: code is too specific. İn formal specification you usually don't specify that detailed but you specify the general behaviour of the system. So usually the specification corresponds to a lot of programs with subtle differences. That's why code a documentation falls short: you don't know what is intentional and what is just a random choice. It's simply too specific to describe high level requirements. The other way around (verification of program with respect to the specification) can be more feasible to implement.