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

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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe