4 ms·
I think the issue with the way people try to promote the use of formal methods, is that they assume that people will want to model their system formally before
by microcolonel 8y ago
I think the issue with the way people try to promote the use of formal methods, is that they assume that people will want to model their system formally before implementing it.
I feel like there'd be more productivity in showing people what their code could do, and helping them narrow that down to what it should. It is, of course, hard to do this.
- kiriakasis 8y agoFrom this point of view I like TLA+, it gives you a simple but powerful programming language and then allows you to check stuff like "this must not happen" or "this must happen" (and more). Formal proof as in coq-proof are often not reasonable for many dynamic projects