Slashdot Mirror

Not the first and not the last project like this. To mention just 2:
HaLVM
Mirage

There are similar projects for OCaml (http://openmirage.org/) and Haskell http://corp.galois.com/halvm as well as some dull activity with Java VM in the same direction. I believe, that this approach is the future, since it simplifies (a lot) building and management of elastic cloud-based applications.

But I would contend that it's still pretty tough stuff to get that right. You gotta consider how good your compiler is, how good your C library is, the numerical stability of the algorithms for your platform, etc.In fact, if you think too much about it, you're probably gonna become one über paranoid kind of dude. At least one very well know book on crypto is said to have very buggy code.

As a matter of fact, the US Government has a bunch of Haskell hackers under contract to develop mathematically proven, type-safe crypto protocols. They are Galois

The experimental Tearline Wiki system we've developed at Galois might suit your needs. Inside the firewall, you use MediaWiki with the Tearline system, and get a combined view of your internal wiki(s), possibly different wikis on different sub-nets, and you can integrate it with Wikipedia or other internet-based wikis to get the global context of the article.

As others have said, integrating your content with other people's content can be a legal issue.

Contact me if you want more information on Tearline :)

peace,

    isaac

The experimental Tearline Wiki system we've developed at Galois might suit your needs. Inside the firewall, you use MediaWiki with the Tearline system, and get a combined view of your internal wiki(s), possibly different wikis on different sub-nets, and you can integrate it with Wikipedia or other internet-based wikis to get the global context of the article.

As others have said, integrating your content with other people's content can be a legal issue.

Contact me if you want more information on Tearline :)

peace,

    isaac

But that just raises the question of how to define a hash function mathematically? The lambda calculus, Godel Numbers? Things like cryptographic hash functions don't tend to be nice algebraic thingies like f(x)=x*x+7, especially since they're usually iterative and deliberately messy - the pretty functions are likely to be less secure.

On the other hand, there are things like cryptol in which you may be able to specify hash functions more mathematically. For example, here is a cryptol implementation of skein.

But that just raises the question of how to define a hash function mathematically? The lambda calculus, Godel Numbers? Things like cryptographic hash functions don't tend to be nice algebraic thingies like f(x)=x*x+7, especially since they're usually iterative and deliberately messy - the pretty functions are likely to be less secure.

On the other hand, there are things like cryptol in which you may be able to specify hash functions more mathematically. For example, here is a cryptol implementation of skein.

That wasn't intentional. I think I must not have enclosed the "a href" tag properly. Here, let me try again.

I assure you that there really is such a company; I have visited their offices on several occasions.

There's some documentation on Galois' web page. I looked at it once awhile back, and it seemed a lot like Haskell, but with extra syntax for doing common cryptographic operations.

Chapter 8 of the programming guide has example cryptol implementations of DES, RC5, and AES.

There's some documentation on Galois' web page. I looked at it once awhile back, and it seemed a lot like Haskell, but with extra syntax for doing common cryptographic operations.

Chapter 8 of the programming guide has example cryptol implementations of DES, RC5, and AES.

Clarification:

Cryptol, as I understand it, was developed by Galois (who, for some reason, is not mentioned in the summary) and not by the NSA. It would be interesting to know whether it was a joint decision between Galois and the NSA to release cryptol, or just Galois' decision alone.

First, the author is not against open source. In fact, Coverity is helping projects like FreeBSD by providing tools for developers.

Second, he is not comparing apples to oranges. He is using a metric, bug-rate in a wide sample. Then, he finds, interestingly enough, that proprietary software is very much scattered, but the ones on the top are 5 X less buggy than open source. This begs the question: why? This is what people should be discussing. Not saying he works for Microsoft and all that childish bullshit...

The *real* question is: what are those methods people developing mission-critical software use that open source hackers do not? My hunch is: formal methods, safe languages.

For instance, Ocaml http://www.astree.ens.fr/ was used in a sofware verification system for the Airbus A340 fly-by-wire system. Haskell is used by Galois Connection http://www.galois.com/ to develop secure protocols for the DoD. And there are many other examples, just look at the clients of vendors of Erlang (well known), Common Lisp, and Eiffel.

As long as the open source community sticks to C (and C++), we're all going to remain in this ridiculous situation that we are in today. In this day and age you can use a fast compiler for safer languages like ML, Lisp or Eiffel, but people insist programming like we're in the 70s.

I sometimes suspect that .NET may be the only hope of getting functional programming adopted by the maininstream.

Haskell is available for .NET now, using Mondrian.

Or, you can can access the Framework's libraries with Hugs98 for .NET.

Who would have though that a mainframe manufacturer would keep prompting dead langauges? <g>

Whilst Algol isn't there, Oberon is, as is Ada, a shareware version of Forth, Haskell, Eifell, Pascal, Perl, Python (twice) and SmallTalk

Who would have though that a mainframe manufacturer would keep prompting dead langauges? <g>

Whilst Algol isn't there, Oberon is, as is Ada, a shareware version of Forth, Haskell, Eifell, Pascal, Perl, Python (twice) and SmallTalk

However when they came to try to port something like haskal over to it, they found it just wouldn't fit(See page 18) so they had to make do with a sort of bridge instead.

So what I think they've done is taken a functional language, taken out the features that don't fit well with .net (untyped terms?) and called it a "feature" :)

I'm way out of my depth on this though - hopefully by providing links someone cleverer than me will correct me.