[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

[Gerwin Klein]

Florian Haftmann wrote:
> A) Archaic, hardly readable and fragile proof techniques:
>   * unfolding definitions of predicates over logical formulae instead of
>     proper intro/elim-rules

There was some discussion on this already, and I'd agree with Tobias and Amine 
that it's just a matter of taste. Having intro/elim rules can be more brittle 
than unfolding.


>   * long apply-Scripts with sometimes obscure tacticss

Indeed, I don't like these either. Some of them go back to the time of ML 
scripts. I don't see the value in investing a lot of time into making them 
beautiful, though. No-one wants to read them. The only reason would be to make 
maintenance easier, but it didn't seem to be a problem so far.


> B) Naive use of locales (instead of proper interpretation):
>   * somehow arbitrary mixed explicit locales and simple predicates
>   * free-floating use of uninterpreted global rules from locales
>   * use of "defines", where definition etc. would be appropriate

Dude ;-) These things were written when locales didn't even fully exist yet. 
It is the first substantial use of the idea (hence the use of "open", which 
was the only kind of locale that existed at the time). Of course they're not 
using interpretations, we hadn't even thought of the concept yet (in fact, I 
believe that we started discussing them because of this application), and 
definition was something I'd very much have liked to have (and also suggested 
at the time) but it was still many years too early.

In short: you're perfectly right, with modern locales this could be written a 
lot nicer. At the time it was as good as it got, though. I'm perfectly fine 
with someone going over these and making them into proper locales. I'm not 
volunteering, though ;-)


> C) A lot of forked (but not shared) theories in MicroJava, Jinja,
> JinjaThreads.
> 
> Of course, all these are due to historic reasons, layers of increasing
> state of the art built on top of each other.  Anyway, concerning C),
> IMHO in the future we should try harder to avoid such duplication by
> distilling reasonable libraries out of large-sized projects.  E.g. these
> projects contain independent developments of semilattices, work which
> would fit more appropriately in HOL-Algebra and then could simply be
> re-used.  Such shared libraries would greatly increase the motivation
> and benefit for keeping them technically at the height of the day than
> such (superficially) "specialized" and "adapted" theories scattered over
> different projects.

Quite right. The problem with that is that it costs considerable time and when 
your focus is the large project and not the distribution, you will just not 
care enough to do it. We should get into the habit of explicitly allocating 
time for activities like that.

Cheers,
Gerwin