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

[Burkhart Wolff]

Hm, ich wusste nicht, das nur “Developer” mit dem Prädikat 
IMG (in München gewesen) Beiträge an den Isabelle Bibliotheken
leisten können sollen dürfen. Auch wenn das der Isabelle Philosophie
von Code-follows-Function zuwider läuft wie in diesem Fall.

Da erscheint Larrys Anregung, gewisse Bibliothekskomponenten
in die AFP auszulagern in einem neuen (und vielleicht unerwuenschtem) Licht.



Nun ja, schade. Um so wichtiger wird es, das die AFP zukünftig 
Mechanismen hat, wie auch Isabelle Komponenten zugelassen werden 
koennen. Vielleicht ist das ja in der Tat der bessere Weg.

@Makarius/Florian: Gibt es diesbezüglich  Neuigkeiten ?
Sollte man eine docker-aehnliche Infrastruktur in der AFP haben ?

Liebe Grüsse aus dem sonnigen Paris,

bu



> Begin forwarded message:
> 
> From: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
> Subject: Re: [isabelle-dev] New Code Generator Target: F#
> Date: 25 August 2022 at 08:27:27 CEST
> To: Tobias Nipkow <nipkow at in.tum.de>, "Achim D. Brucker" <adbrucker at 0x5f.org>, Isabelle-Development Mailinglist <isabelle-dev at in.tum.de>
> 
>> 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220825/a0e5e501/attachment.htm>