4 ms·

Interesting. I think the point about the mathematics being too difficult for a "rank and file" programmer is probably a little off base. It isn't so much that

by jaziek 11y ago

Interesting. I think the point about the mathematics being too difficult for a "rank and file" programmer is probably a little off base. It isn't so much that the concepts are difficult as the fact that it seems prohibitively time consuming for relatively little gain that would put most people (especially those managing a project) off using formal specification / verification to build their software. In most cases besides safety critical systems, it is acceptable to ship a product in 1/10th of the time, knowing that there is chance that there are imperfections. Additionally, having used the Z language mentioned in the article, and taken some classes in university on formal methods, the thing which put me off the most was the (necessary) verbosity of the specification languages that are used for these type of things. I never wrote something that wasn't incredibly trivial, because it would have taken too long.

Jafit 11y ago
"1/10th of the time" implies that it takes 10 times longer to do the math than it does to stare at the screen with your head in your hands saying "oh god what have I done?" to yourself. I'd wager that's not the case.
DennisP 11y ago
As a rank and file programmer who didn't take university classes on formal methods, I've found it pretty difficult to dig up accessible tutorials.
- mannykannot 11y ago
  This wasn't my introduction to these methods, but I wish it was: http://www.amazon.com/Error-Free-Software-Know-How-Correctness-Engineering/dp/0471930164 http://www.amazon.com/Error-Free-Software-Know-How-Correctne...
mannykannot 11y ago
It's a paradigm shift compared to the usual approach to programming, so I don't think it is for everybody, and realistically, it doesn't have to be. For me, the most useful thing about learning some of this is that while I never, in practice, do fully formal proofs, I make informal arguments for correctness as I write and I think about what it would take to formalize them - what is the invariant, preconditions etc. here? For the tricky bits, I will write out an informal argument for correctness and include it as a comment. According to the article, Praxis is not using formal proofs exclusively, or even predominately, and is using Z mainly for the precise expression of ideas, while keeping them free of unnecessary implementation detail (in other words, for abstraction.)

by jaziek 11y ago

Jafit 11y ago

"1/10th of the time" implies that it takes 10 times longer to do the math than it does to stare at the screen with your head in your hands saying "oh god what have I done?" to yourself. I'd wager that's not the case.

DennisP 11y ago

As a rank and file programmer who didn't take university classes on formal methods, I've found it pretty difficult to dig up accessible tutorials.

mannykannot 11y ago
This wasn't my introduction to these methods, but I wish it was: http://www.amazon.com/Error-Free-Software-Know-How-Correctness-Engineering/dp/0471930164 http://www.amazon.com/Error-Free-Software-Know-How-Correctne...

mannykannot 11y ago

It's a paradigm shift compared to the usual approach to programming, so I don't think it is for everybody, and realistically, it doesn't have to be. For me, the most useful thing about learning some of this is that while I never, in practice, do fully formal proofs, I make informal arguments for correctness as I write and I think about what it would take to formalize them - what is the invariant, preconditions etc. here? For the tricky bits, I will write out an informal argument for correctness and include it as a comment. According to the article, Praxis is not using formal proofs exclusively, or even predominately, and is using Z mainly for the precise expression of ideas, while keeping them free of unnecessary implementation detail (in other words, for abstraction.)