Galchin Vasili wrote on Friday, January 4:

...

I stumbled across this page. It seems that Haskell and other strongly typed functional languages like Ml/OCaml will fare much, much better, e.g. buffer overrun. Thoughts . .... comments.

Bulat Ziganshin wrote:

for me, it looks like saying that haskell better uses CPU registers :) the truth is that modern languages (including Java/C#) doesn't use buffers directly. i don't have experience of their usage, but for Haskell i had memory referencing problems only when using unsafe* tricks

Interestingly enough, a few days after this exchange, the first public report was released from a large survey funded by US Homeland Security on security of open source projects. The survey was carried out by a company called Coverity. Among the projects making top grade for security - apparently far better than most proprietary products, though complete information about that is not public - were PHP, Perl, and Python. PHP? Come on, can't we do at least as well? But right now, there is a technical impediment to the participation of Haskell: the Coverity project currently only supports projects written in C, C++, and Java. Haskell compilers are often written in Haskell. Any ideas? Perhaps Coverity's interest could be piqued if they were made aware of Haskell's emergence as an important platform in security-sensitive industries such as finance and chip design, and of the significant influence that Haskell is having on the design of all other major programming languages. The home page for the Coverity open source project is at: http://scan.coverity.com/ Some recent press coverage: http://it.slashdot.org/article.pl?sid=08/01/09/0027229 http://www.zdnet.com.au/news/security/soa/11-open-source-projects-pass-secur... http://www.informationweek.com/story/showArticle.jhtml?articleID=205600229 -Yitz

Bryan O'Sullivan wrote:

Yitzchak Gale wrote:

...

Perhaps Coverity's interest could be piqued if they were made aware of Haskell's emergence as an important platform in security-sensitive industries such as finance and chip design, and of the significant influence that Haskell is having on the design of all other major programming languages.

During one of Simon PJ's tutorials at OSCON last year, a Coverity engineer was in the audience. He told us afterwards that he downloaded the GHC source and gave a try at analysing it while Simon talked. He didn't get far, of course; their software wasn't built for the tricks that -fvia-C plays. But they have at least one person who was that interested.

unregisterised, it should be standard C without tricks, though still nothing like ordinary C and therefore possibly not analyzable ~Isaac

Hi, Andrew Coppin wrote:

Galchin Vasili wrote:

...

Hello,

https://buildsecurityin.us-cert.gov/daisy/bsi/articles/knowledge/coding/295....

I stumbled across this page. It seems that Haskell and other strongly typed functional languages like Ml/OCaml will fare much, much better, e.g. buffer overrun. Thoughts . .... comments.

Human kind has yet to design a programming language which eliminates all possible bugs. ;-) And we never will. See http://en.wikipedia.org/wiki/Halting_problem .

Greetings, Mads

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

Am Sonntag, 6. Januar 2008 14:27 schrieb Mads Lindstrøm:

Hi,

Andrew Coppin wrote:

...

Galchin Vasili wrote:

...

Hello,

https://buildsecurityin.us-cert.gov/daisy/bsi/articles/knowledge/coding /295.html

I stumbled across this page. It seems that Haskell and other strongly typed functional languages like Ml/OCaml will fare much, much better, e.g. buffer overrun. Thoughts . .... comments.

Human kind has yet to design a programming language which eliminates all possible bugs. ;-)

And we never will. See http://en.wikipedia.org/wiki/Halting_problem .

Greetings,

Mads

Just because I don't know: what bugs would be possible in a language having only the instruction return () (';' for imperative programmers)? Cheers, Daniel

Am Sonntag, 6. Januar 2008 15:18 schrieb Andrew Coppin:

Daniel Fischer wrote:

...

Just because I don't know: what bugs would be possible in a language having only the instruction return ()

Bug #1: You cannot write any nontrivial programs. ;-)

That's not a bug, that's a feature.

Achim Schneider wrote:

That's an interesting task: Design a non-touring complete, restricted language in which every expression is decidable, without making the language unusable for usual programming problems.

Have a look about dependently typed languages like Epigram: http://www.e-pig.org/ Regards, apfelmus

On Sun, 2008-01-06 at 16:19 +0100, Daniel Fischer wrote:

Am Sonntag, 6. Januar 2008 15:54 schrieb Achim Schneider:

...

Daniel Fischer wrote:

...

Am Sonntag, 6. Januar 2008 15:18 schrieb Andrew Coppin:

...

Daniel Fischer wrote:

...

Just because I don't know: what bugs would be possible in a language having only the instruction return ()

Bug #1: You cannot write any nontrivial programs. ;-)

That's not a bug, that's a feature.

That's an interesting task: Design a non-touring complete, restricted language in which every expression is decidable, without making the language unusable for usual programming problems.

I'm not a logician, but didn't Gödel prove that you couldn't express the (full) arithmetic of natural numbers in such a language? Of course it might be possible to express a sufficiently interesting part of it, but I should be surprised.

What Goedel meant by "arithmetic" is a bit more than one usually associates with the term. One person mentioned Epigram. Most theorem provers and most? (of the few) dependently typed programming languages would fit Achim's criterion depending on the range of "usable" and "usual". Coq, for example, is likely to be capable of formalizing just about anything you'd want. Of course, there is one class of "programming problem" that we can already say can't be handled; namely implementing interpreters (for Turing complete languages). We can formalize analyses, make compilers, prove the compilers correct with respect to a semantics, and even prove that a -description- of an interpreter correctly implements the semantics, but we can't actually -run- the interpreter.

Daniel Fischer wrote:

Am Sonntag, 6. Januar 2008 15:54 schrieb Achim Schneider:

...

That's an interesting task: Design a non-touring complete, restricted language in which every expression is decidable, without making the language unusable for usual programming problems.

I'm not a logician, but didn't Gödel prove that you couldn't express the (full) arithmetic of natural numbers in such a language?

What if you restricted yourself to the arithmetic of natural numbers modulo 2^64?

That's an interesting task: Design a non-touring complete, restricted language in which every expression is decidable, without making the language unusable for usual programming problems.

Well, I did something like that a few years ago - it was a sort of assembler language, allowing the programmer to, say, sort an array, but not to calculate Akkerman function.

Am Sonntag, 6. Januar 2008 20:04 schrieb Miguel Mitrofanov:

...

That's an interesting task: Design a non-touring complete, restricted language in which every expression is decidable, without making the language unusable for usual programming problems.

Well, I did something like that a few years ago - it was a sort of assembler language, allowing the programmer to, say, sort an array, but not to calculate Akkerman function.

Epigram even allows you Ackermann’s function. Best wishes, Wolfgang

Mads Lindstrøm wrote:

Andrew Coppin wrote:

...

Human kind has yet to design a programming language which eliminates all possible bugs. ;-) And we never will. See http://en.wikipedia.org/wiki/Halting_problem .

If you limit usage of general recursion (and rather favor structural recursion) then you can mitigate the halting problem. But there always will be specification bugs (when one implenetes something else than what was needed). Peter.