[isabelle-dev] New Code Generator Target: F#
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 25 08:27:27 CEST 2022
> 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
> 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
>>> 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
>>> environment variable - i.e., without the sandboxed dotnet
>>> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev