[hcs-d] Summer Development Projects (and a virtual meeting
smanek at gmail.com
Tue Jul 1 19:17:43 EDT 2008
-----BEGIN PGP SIGNED MESSAGE-----
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
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.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
-----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
More information about the hcs-discuss