[Haskell-cafe] www.galois.com vs Google??

[Vasili I. Galchin]

Hello Haskellers(and all FPL people),

I just ran across the following effort by Google:
http://blogs.techworld.com/war-on-error/2014/07/googles-project-zero-flaw-programme-do-gooding-spin-or-a-much-needed-evolution/index.htm

It seems to me that www.galois.com(www.janestreetcapital.com)
realizes that the solution to software correctness problems doesn't
lie with uncontrolled "mutability" ...

Question: does Google concur with www.galois.com or google's
effort just "more of the same"??

Vasili
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Vasili I. Galchin]

Tobias,

I pretty agree with your response. I was trying to challenge the
entire audience to think about the issue about software
correctness(e.g. strong typefullness (and static type checking) like
Haskell, et. al. vs no type-checking/ dynamic type checking). My point
is how can we as a community respond to Google's challenge?? In my
humble opinion (IMHO) I think Google has missed the point regarding
contemporary software correctness problems .. (and also the Tor
project . given the languages of implementation) ..

Here is a very simple and cheesy example .. I worked at HP on a
contract .. . a predecessor of mine used with typefullnes of C++ (I
thinking using type casting ) and did a buffer overrun of "heap"
allocated that corrupted "the heap allocator metadata" (malloc) ....
of course I used to "gdb" to do a "postmordum after the patient died"
... IHMO I would been more happier if this "overrun" had been detected
at compile-tyime .. due to static strong type checking ... :-)

Alll grammer errors are due to my cat Buddy ...

Vasya

On Thu, Jul 31, 2014 at 5:24 AM, Tobias Dammers <tdam...@gmail.com> wrote:
> The way I read that article, those are two very different goals and
> approaches.
>
> The "Project Zero" thing seems to be about subjecting "everything" to
> thorough security checking by the best experts Google can buy, in order
> to fix as many security problems on the internet as they possibly can.
>
> The software correctness problem is somewhat related, but not entirely -
> not all security problems are software bugs, and not all software bugs
> are security problems.
>
> On a side note, I think both problems are inherently unsolvable - we can
> go a long way cleaning up the solvable problems, and building an
> infrastructure that avoids them by design, but some potential for bugs
> and flaws will always remain, at least as long as we're using reasonable
> definitions of "programming" and "software".

[Tobias Dammers]

I believe that ultimately the answer lies in applying both strategies.

Provable correctness is great, and it helps keep truckloads of
headdesk-worthy oversights out the door, and a strict static type system
keeps good programmers honest - but people still make mistakes, design
oversights, or just implement the wrong thing correctly. That kind of
bug can never be caught through formal / technical means: even in the
most rigid formal type system, you can still implement things based on
wrong assumptions, and all the type system will do for you is confirm
that the code you wrote matches your wrong assumptions.

OTOH, that doesn't mean we should let go of static checks altogether -
that's as silly as saying we shouldn't wear seatbelts because they don't
save *all* lives in traffic accidents. Static checks are useful to weed
out something like 99% of the stupid mistakes people make all the time;
for the remaining 1%, we still need manual labor and scrupulous auditing
and pen-testing. The part where you check whether the real-world
assumptions that your code is based on are actually valid is something
we cannot possibly automate - we'd need a machine with full
understanding of the real world to do that.

Oh, and just to make this clear: when I say "static type checker", I am
here talking about the concept in the widest possible sense, including
unit test suites (which, if you think about it, are just another way of
implementing an ad-hoc static type system), static code analyzers,
coding style checkers, etc.