[isabelle-dev] Notes on GHC an mutable data structures

Makarius makarius at sketis.net
Tue Oct 6 19:33:45 CEST 2015

On Tue, 22 Sep 2015, Florian Haftmann wrote:

> http://www.aosabook.org/en/ghc.html, section starting with »Crime 
> Doesn't Pay« – from The Architecture of Open Source Applications (Volume 
> 2): The Glasgow Haskell Compiler

That is indeed a very interesting document.  About half of the points 
apply equally well to the Isabelle code base.  For example:

   We obsessively refactor while adding new code, keeping the code base as
   fresh as possible.

Later there are more explanations how the ultra strong type-discipline of 
Haskell helps in the process.

Compared to that, the code base of Java SE is just one big bog of legacy 
code.  For me, the historical argument if OO-programming has significant 
solutions to the perpetual "software crisis" is over.


More information about the isabelle-dev mailing list