[hcs-d] Summer Development Projects (and a virtual meeting tonight!)

Shaneal Manek smanek at gmail.com
Tue Jul 1 19:17:43 EDT 2008

Hash: SHA1

A 'verified' program is one that is, in some sense, proven to work.

At a high level, computer programs can be thought of as analogous to
mathematical  functions that maps a set of inputs to a set of outputs
. Hence, if you can prove that the program produces desirable output
for any input, you have proved its correctness and effectively
'verified' it.

Obviously, this is ridiculously time consuming (and hence expensive)
to do for all but the most trivial of programs so no one, save NASA
and a few other similar large agencies, actually do it.

Haskell is ostensibly a purely functional programming language
(ignoring cheating with monads and the like for a moment). It's
nominally easier to verify a purely functional program, since there
are no side effects - and hence an easier execution path to trace.
It's also a rather difficult language to learn (for me at least) ...

So, if I am grokking Josh's original email, it was basically just a
joke :-) Just an effectively impossible task.

- -Shaneal
Version: GnuPG v1.4.6 (GNU/Linux)


On Tue, Jul 1, 2008 at 6:29 PM, Ivan Krstić
<krstic at solarsail.hcs.harvard.edu> wrote:
> On Jul 1, 2008, at 1:56 PM, Joshua Kroll wrote:
>> writing verified web servers in Haskell*,
> What does this mean?
> --
> Ivan Krstić <krstic at solarsail.hcs.harvard.edu> | http://radian.org
> _______________________________________________
> hcs-discuss mailing list
> hcs-discuss at lists.hcs.harvard.edu
> http://lists.hcs.harvard.edu/mailman/listinfo/hcs-discuss

More information about the hcs-discuss mailing list