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

[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.

On Fri, Aug 01, 2014 at 03:53:04AM -0500, Vasili I. Galchin wrote:
> 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 <tdammers at 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".
> >
> > On Wed, Jul 30, 2014 at 10:08:06PM -0500, Vasili I. Galchin wrote:
> >> 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
> >> Haskell-Cafe at haskell.org
> >> http://www.haskell.org/mailman/listinfo/haskell-cafe