3 ms·

I think you're making a good point, but your tone is unnecessarily strident.

by chubot 8y ago

Jtsummers 8y ago
I'll disagree, I don't think they're making a good point. GP implies that formal methods always add time to projects, which is going to be true for: 1) Projects that are building the wrong thing and spend time verifying the wrong thing (failed validation) 2) Projects with people inexperienced in formal methods (most projects today) The latter is just a matter of experience. Once people get used to thinking about things in a more formal way, they'll get faster. Additionally, they'll learn which parts need to be shown formally and which don't (or which parts they can show via their type system versus those which need to be modeled outside the language and type system, etc.). I don't need to formally prove that my program writes message X to memory block Y, it can be verified by: inspection, tests. I do want to prove that my two processes correctly exchange messages (since the nature of the system is such that we needed to write our own protocol rather than being able to rely on a pre-built and verified/validated one). But here I'm proving the protocol, I still have to test the implementation (unless my language permits me to encode proofs in a straightforward way). The former is a separate issue from formal methods. It's failed validation efforts which is solved (or mitigated) by something else: lean/agile approaches to project management (versus delaying feedback from customers, and consequently delaying validation activities).
- verinus 8y ago
  well if I read you correctly he IS making a good point: > 2) Projects with people inexperienced in formal methods (most projects today) which is exactly what matters and what adds a lot of time to dev. 1) cannot be addressed by formal method and is one of the most important things when building software.
  - Jtsummers 8y ago
    It’s a temporary problem, not a permanent problem. People need training and practice. I’d expect most people were slower when first using unit tests or TDD than they are today. It takes time to build that experience into the industry but it’s hardly an impossible problem. Especially as the tooling (PlusCal, Alloy) for lighter weight formal methods gets better and more accessible.

I think you're making a good point, but your tone is unnecessarily strident.

by chubot 8y ago

I think you're making a good point, but your tone is unnecessarily strident.

I'll disagree, I don't think they're making a good point. GP implies that formal methods always add time to projects, which is going to be true for: 1) Projects that are building the wrong thing and spend time verifying the wrong thing (failed validation) 2) Projects with people inexperienced in formal methods (most projects today) The latter is just a matter of experience. Once people get used to thinking about things in a more formal way, they'll get faster. Additionally, they'll learn which parts need to be shown formally and which don't (or which parts they can show via their type system versus those which need to be modeled outside the language and type system, etc.). I don't need to formally prove that my program writes message X to memory block Y, it can be verified by: inspection, tests. I do want to prove that my two processes correctly exchange messages (since the nature of the system is such that we needed to write our own protocol rather than being able to rely on a pre-built and verified/validated one). But here I'm proving the protocol, I still have to test the implementation (unless my language permits me to encode proofs in a straightforward way). The former is a separate issue from formal methods. It's failed validation efforts which is solved (or mitigated) by something else: lean/agile approaches to project management (versus delaying feedback from customers, and consequently delaying validation activities).

verinus 8y ago
well if I read you correctly he IS making a good point: > 2) Projects with people inexperienced in formal methods (most projects today) which is exactly what matters and what adds a lot of time to dev. 1) cannot be addressed by formal method and is one of the most important things when building software.
- Jtsummers 8y ago
  It’s a temporary problem, not a permanent problem. People need training and practice. I’d expect most people were slower when first using unit tests or TDD than they are today. It takes time to build that experience into the industry but it’s hardly an impossible problem. Especially as the tooling (PlusCal, Alloy) for lighter weight formal methods gets better and more accessible.