Hi Achim and Tobias &al., > I would appreciate your general opinion on F# as a new code generator target > and, > in particular, your opinion and recommendations on future > maintenance/development > models. I see, in principle two approaches: > > 1) integrating it into the main distribution of Isabelle or > 2) keeping it as a separate "component" (theoretically, it could even be an > AFP > entry, if users install dotnet themselves and configure the > ISABELLE_DOTNET > environment variable - i.e., without the sandboxed dotnet installation)
> the code generator is part of Isabelle's trusted infrastructure. Thus I
> recommend you provide your F# code generator as an AFP entry in the Tools
> category.
IMHO this argument on its own does not apply here. The code generator
is modular: adding another target language does not
affect existing target languages and hence does not affect their
trustworthiness, particularly not of Isabelle/ML (»Eval«)
which is at the core of all proof-replacing evaluation mechanisms.
Concerning trustworthiness in general, the code generator by its
architecture can never achieve the trustworthiness of e. g.
the LCF-style inference kernel: you are always free to configure
pointless or »unsound« things, sometimes burdening
users to come up with an appropriate »interpretation« what generated
code means in relaton to its originating theory;
a prominent example from the distribution is
HOL/Library/Code_Real_Approx_By_Float.thy.
Hence from my perspective it is difficult to argue that there are
fundamental differences between distribution
and AFP concerning trustworthiness of code generation.
From a maintenance perspective, integration into the distribution seems
actually to be the more appropriate way:
we have the tradition to setup target-language specific things in
theories where their corresponding logical
notions comes up (e. g. List.thy), and this makes things easier to
maintain and re-check across all target languages.
There might still be other issues suggesting the AFP.
Cheers,
Florian
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
