3 ms·

I think formal methods may take off sometime in the future, hopefully not too distant from now. But this has been a thing since the mid 90s, and tools might sti

by nextos 7y ago

I think formal methods may take off sometime in the future, hopefully not too distant from now. But this has been a thing since the mid 90s, and tools might still not be mature enough. I did a whole MSc in Formal Methods about a decade ago, and I think abstract interpretation, model checking and axiomatic specifications are ready for prime time now. Exotic type systems and theorem provers are still a bit costly to use, but have achieved some spectacular successes like seL4. I guess JetBrains wants to be in this space once things mature.

im_down_w_otp 7y ago
The reason I'm so excited about this development is that it's a commercial product-focused company putting a level of effort into polish and refinement into this domain. The lack of that kind of polish is an enormous inhibitor to adoption and acceptance of these classes of tools. Most, not all, formal methods tools are a tire fire of incoherent UX, bespoke Byzantine runtime requirements, and scattered piecemeal documentation & tutorials. Which makes complete sense when you consider where they originate, what they're typically used for, how they're maintained, and who their subset of end users are. You have to reeeeaaaalllly need to reach for one of these tools to put up with how bad they are, and the population of developers who have that need is significantly smaller than the population who could derive some value & benefit from the methods were they not also unnecessarily painful to use on top of their already being conceptually challenging for the uninitiated. Their niche status becomes self-perpetuating. A company like JetBrains making a move like this might stand a chance of breaking the logjam.
mcguire 7y ago
For a look at the state of non-dependently typed formal methods, take a look at Frama-C and Ada Spark. Frama-C is pretty rough around the edges (and both have some significant limitations) but is amazingly useful while Spark is more constrained but has much better tooling. A language (like Dafny?) with garbage collection plus the techniques behind those two would make for a very powerful toolset.

by nextos 7y ago

im_down_w_otp 7y ago

The reason I'm so excited about this development is that it's a commercial product-focused company putting a level of effort into polish and refinement into this domain. The lack of that kind of polish is an enormous inhibitor to adoption and acceptance of these classes of tools. Most, not all, formal methods tools are a tire fire of incoherent UX, bespoke Byzantine runtime requirements, and scattered piecemeal documentation & tutorials. Which makes complete sense when you consider where they originate, what they're typically used for, how they're maintained, and who their subset of end users are. You have to reeeeaaaalllly need to reach for one of these tools to put up with how bad they are, and the population of developers who have that need is significantly smaller than the population who could derive some value & benefit from the methods were they not also unnecessarily painful to use on top of their already being conceptually challenging for the uninitiated. Their niche status becomes self-perpetuating. A company like JetBrains making a move like this might stand a chance of breaking the logjam.

mcguire 7y ago

For a look at the state of non-dependently typed formal methods, take a look at Frama-C and Ada Spark. Frama-C is pretty rough around the edges (and both have some significant limitations) but is amazingly useful while Spark is more constrained but has much better tooling. A language (like Dafny?) with garbage collection plus the techniques behind those two would make for a very powerful toolset.