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

On Feb 17, 2009, at 11:46 PM, John Nowak wrote:

>
> 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.

Agreed. I've never forgotten this lesson from my high school geometry
teacher:

An object is sitting on the teacher's desk at the front of the room.
The problem is to develop a formal procedure that will move the
object from there to the southwest corner of the room. Easy enough...

Then the teacher says to repeat the problem with the object sitting
on the floor next to the teacher's desk. The only acceptable answer
is to pick up the object and place it on the desk -- the rest of the
problem is already solved!

Now, while this method of problem solving can be used in any
programming language, concatenative languages are built upon
this foundation. So, concatenative languages enable a programmer
to use provably-correct formal methods by their very nature.
--
don


> - John