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

[Tobias Nipkow]

The code generator is sensitive. Having an external contribution in the AFP 
clearly delineates what comes from the core developers and what not.

Tobias

On 23/08/2022 18:13, Florian Haftmann wrote:
> 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: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220823/95575a41/attachment-0001.bin>