Python from Wise Guy's Viewpoint

[Matthias Blume]

Joachim Durchholz <joachim.durchholz at web.de> writes:

> Pascal Costanza wrote:
> > ....because static type systems work by reducing the expressive
> > power of a language. It can't be any different for a strict static
> > type system. You can't solve the halting problem in a
> > general-purpose language.
> 
> 
> The final statement is correct, but you don't need to solve the
> halting problem: it's enough to allow the specification of some
> easy-to-prove properties, without hindering the programmer too much.

In fact, you should never need to "solve the halting problem" in order
to statically check you program.  After all, the programmer *already
has a proof* in her mind when she writes the code!  All that's needed
(:-) is for her to provide enough hints as to what that proof is so
that the compiler can verify it.  (The smiley is there because, as we
are all poinfully aware of, this is much easier said than done.)

Matthias