user2342

"Muss man wissen!"

Interesting! What are Bonsai's dependencies? I use OCaml but - so far - none of Janestreets libraries etc.

> For example, clang defines __GNUC__=4 (and __GNUC_MINOR__=2, __GNUC_PATCHLEVEL__=1) to claim compatibility with GCC 4.2.1.

Is this because Apple at some point stopped updating GCC because of the GPL license change? I think GCC 4.2.x was the last GCC licensed under GPLv2. Could be for compatibility reasons for Mac software.

I fully agree with the article, but the snow effect on the site is more distracting to readability than the shitty menu icons in Tahoe...

It's there, but yes the home page is very confusing. I lost interest very fast.

Weak arguments in the article with badly chosen examples.

If one wanted to criticize OCaml syntax, the need for .mli-files (with different syntax for function signatures) and the rather clunky module/signature syntax would be better candidates.

Thanks. Looks promising!

Rather for the classic 3x3x3 cube. I played with it in the 80ies, but never understood the concepts behind it.

Are there recommendable sources on how to learn solving/the concepts of a classic cube?

Perhaps a helpful addition: I collected my change money over several years (about 9kg in total, mostly lower valued coins, since the higher values can be spent easily).

After exchanging them on a bank into useful money: the average Euro coin weights about 3.6 grams and has an average value of 7 cents. :-)

Yes, that was my first thought too. The concept is similar.

Get rid if the source-files and put every function/method in its own "editor". However, as far as I remember navigation to/from callers was not possible in Smalltalk.

I'm using Sublime Text since shortly before 2.0 and Sublime Merge since day one. Yet, I'm slowly losing interest in ST because of lacking language integrations and probably won't do any future paid upgrades. However, Sublime Merge is still essential for me and a no-brainer.

> My understanding is that the primary purpose of CompCert is to make formally verified code that is extracted into C also get compiled by a compiler that is formally verified to preserve the intended semantics.

Thats my understanding too. Code is written in high level systems generating C as output. C becomes rather an implementation detail in a hopefully, more or less completely verified tool chain.

They may work as expected (and probably will), but they are not covered by the proof.

Yes, I know, I mentioned the extraction.

My question was whether it can help detecting translation errors from the first step.