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

[Tobias Nipkow]

On 25/08/2022 08:27, Florian Haftmann wrote:
>> 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.

It sounds to me like this could be overcome by a well-defined interface that 
allows people to add their own code generator.

Tobias

> 	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: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220826/85562626/attachment.bin>