Re: [stack] Advantages of cat, joy ..?

On Feb 16, 2009, at 8:44 PM, Don Groves wrote:

>> What the point of it all ?!
>
> To John's excellent summary below, I would add only one thing,
> which he gets close to but doesn't say explicitly, and that is that
> the primary aim of formal methods is to demonstrate program
> correctness.

That may be the primary aim, but I'm not sure it is the primary  
benefit of such an approach. Designing a language to be amenable to  
formal analysis means that you have to keep things simple. You have to  
throw out ideas or language features that, while perhaps easy to  
implement, are hard to reason about. You have to eliminate or  
carefully take note of anything that might violate your fundamental  
model. You have to develop a syntax that makes proofs easier.

Essentially, designing a language with the aim of making formal  
methods useful to more programmers ensures that your language has its  
head screwed on straight. How many languages have we seen that have  
all sorts of odd corner cases and misfeatures surfacing ten years or  
more after their initial release? Things like Ruby's broken scoping  
would've never happened if there was even a hint of effort towards  
making the language subject to rigorous reasoning.

My point is that even if most programmers will not use formal methods,  
they will still greatly benefit by using a language that makes them  
possible. Such a language is essentially guaranteed to have less  
weirdness and less complexity than a language designed with only a  
nebulous concept of "productivity" in mind.

- John