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

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


-----BEGIN PGP SIGNED MESSAGE-----
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
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)

iD8DBQFIarqvhkBc25UmCW4RAi7bAJ9uYfrbe3fTTrl9REs9syQAJyK7NQCfSTxQ
r0mXbbShuF+AzSaMhNB+tWk=
=qRhW
-----END PGP SIGNATURE-----

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