Erlang rocks (Re: Eppur si sugat)

[Chris Pressey]

On Thu, 29 May 2003 00:58:27 -0700 (PDT)
"Dr.Dr.Ruediger M.Flaig" <flaig@REDACTED> wrote:

> [...]
> So are there any theorem provers for Erlang, as there are for
> Lisp and ML?

Yes, it's called "the human mind" :)

Seriously, I think it's a lot more effective for the programmer to prove
their code to his/herself while writing it, than to prove it
mechanically after the fact.  In fact I think most (good) programmers do
this subconsciously, and testing is part of it, to reassure themselves
that they wrote what they meant to write.

I do think there's room for more verification in Erlang (e.g. inferring
type signatures...) but I think it's more suited to the ground-up
'linting' variety.

Disclaimer: I'm mostly a pragmatist too.

-Chris