Re: [isabelle] How do I do stone age interaction?





On 08.12.2010, at 10:19, Alexander Krauss wrote:

>  To use this, ML code must obey some
> structuring principles, and the most important one is that contexts
> (i.e. values of type Proof.context, theory, or local_theory, depending
> on the application) must be passed around explicitly. Anyone familiar
> with the notion of pure functional programming should find this very
> natural.

I think that this point is a good one and deserves special attention. 
a) You need to pass contexts around in purely functional programming.
b) Most of the time, you don't want to deal with this passing around explicitly. 
A purely functional programming language should deal with this in a natural and pretty way 
(nope, monads are not natural; and they are ugly). If there just were such a language ...

> I think that much confusion comes from confusing (1) and (4). Maybe
> reimlementing (1) in LISP (as in Edinburgh LCF) could solve this
> problem :-)).
> 

Why not try Babel-17 instead of LISP? A new and much refined version of it will come out this Friday, together with a Netbeans plugin :-)

- Steven




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.