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

[Florian Haftmann]

> Having an external contribution in the
> AFP clearly delineates what comes from the core developers and what not.

That could indeed by a criterion, although it sacrifices some aspects of
maintainability.

	Florian


> 
> 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
>>
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

-------------- 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/20220825/67ba78e3/attachment.sig>