[isabelle-dev] New Code Generator Target: F#

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220823/37d907a3/attachment.sig>