[isabelle-dev] New Code Generator Target: F#
florian.haftmann at informatik.tu-muenchen.de
Tue Aug 23 18:13:40 CEST 2022
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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev