[erlang-questions] Runtime checking for types
Mon Apr 25 21:28:59 CEST 2011
On Thu, Apr 21, 2011 at 02:08, Richard O'Keefe <ok@REDACTED> wrote:
> On 21/04/2011, at 2:21 AM, Tony Finch wrote:
> > Sounds like Robert Harper.
> The question Harper tries very hard to evade there is
> "Are there any usable type systems that are sufficiently expressive?"
> The only type systems he blesses are the ones in ML and Haskell.
> As a Haskell programmer, I find ML's type system crippling. (No type
> Relying on ad hoc overloading to deal with + and < ? Feh!)
> And there are enough people who find the Haskell type system limiting that
> Epigram, Cayenne, and Agda exist.
> Make no mistake, a *good* type system *can* do wonders for you.
> See the whole "generic programming" stuff, such as Template Haskell,
> and contrast the elegance of QuickCheck in Haskell (driven by the types)
> with the clunkier version for Erlang.
> At the high end, type systems trail off into things like PVS, where proving
> that a specification is type-correct is a non-trivial exercise. (If anyone
> reading this knows PVS and would give me a bit of hand-holding, I'd
> like to be able to use it; the language is clear enough, but driving the
> theorem prover is very far from obvious.)
I used PVS years ago - we started out by proving that quick sort actually
sorts a list. That is not as easy to prove as one would assume, but it is a
good exercise to start with.
Before we dived into PVS we did some pre-study on deduction systems - if you
have no prior exposure to that I would suggest spending a day reading up on
I have gazed at the PVS web page and it seems to be just as hard core and
terse as I recall it... not many have .ps and .ps.gz versions of their
manuals these days! ;-)
I can only offer my advice above since my practical experience with PVS is
too dated to be of any use to you.
You might also consider Isabelle - one of my university friends did his
Ph.D. using Isabelle since it was in some way easier to work with than PVS.
I just checked up on it and it seems more modern than PVS. It also does code
generation, which is the pinnacle of theoretic computer science: just muddle
around in some higher order logic for some time and when you are done you
have a program that is correct. I might want to try that out one day, but I
do not think the market segment where this can be used and make money is all
that big. My friend tried to do formal methods in the industry for a couple
of years before giving up to become a "regular" software engineer.
On the Isabelle site you will also see SPARK Ada mentioned and that is an
interesting approach to creation of correct software. Never used it myself,
but it might be fun to try out.
> When it comes to writing programs, few things are as straitjackety as
> a language that isn't finished yet (Epigram) or one where persuading
> the compiler your program makes sense requires manual guidance of a
> theorem prover.
> erlang-questions mailing list
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the erlang-questions