<br><br><div class="gmail_quote">On Thu, Apr 21, 2011 at 02:08, Richard O'Keefe <span dir="ltr"><<a href="mailto:ok@cs.otago.ac.nz">ok@cs.otago.ac.nz</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<br>
On 21/04/2011, at 2:21 AM, Tony Finch wrote:<br>
><br>
> Sounds like Robert Harper.<br>
><br>
> <a href="http://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/" target="_blank">http://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/</a><br>
<br>
The question Harper tries very hard to evade there is<br>
<br>
    "Are there any usable type systems that are sufficiently expressive?"<br>
<br>
The only type systems he blesses are the ones in ML and Haskell.<br>
As a Haskell programmer, I find ML's type system crippling.  (No type classes?<br>
Relying on ad hoc overloading to deal with + and < ?  Feh!)<br>
And there are enough people who find the Haskell type system limiting that<br>
Epigram, Cayenne, and Agda exist.<br>
<br>
Make no mistake, a *good* type system *can* do wonders for you.<br>
See the whole "generic programming" stuff, such as Template Haskell,<br>
and contrast the elegance of QuickCheck in Haskell (driven by the types)<br>
with the clunkier version for Erlang.<br>
<br>
At the high end, type systems trail off into things like PVS, where proving<br>
that a specification is type-correct is a non-trivial exercise.  (If anyone<br>
reading this knows PVS and would give me a bit of hand-holding, I'd _really_<br>
like to be able to use it; the language is clear enough, but driving the<br>
theorem prover is very far from obvious.)<br></blockquote><div><br>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.<br>
<br>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 that.<br><br>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! ;-)<br>
<br>I can only offer my advice above since my practical experience with PVS is too dated to be of any use to you.<br><br>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.<br>
 <br>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.<br><br>Cheers,<br>Torben<br> </div>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<br>
When it comes to writing programs, few things are as straitjackety as<br>
a language that isn't finished yet (Epigram) or one where persuading<br>
the compiler your program makes sense requires manual guidance of a<br>
theorem prover.<br>
_______________________________________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
</blockquote></div><br><br clear="all"><br>-- <br><a href="http://www.linkedin.com/in/torbenhoffmann">http://www.linkedin.com/in/torbenhoffmann</a><br>