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

[Tobias Nipkow]

I don't know who you wanted to address when you emailed "Makarius Wenzel 
<isabelle-dev at in.tum.de>", but please use English on this list.

Tobias

On 25/08/2022 12:15, Burkhart Wolff wrote:
> 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 
>> <mailto: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 <mailto:nipkow at in.tum.de>>, "Achim D. 
>> Brucker" <adbrucker at 0x5f.org <mailto:adbrucker at 0x5f.org>>, 
>> Isabelle-Development Mailinglist <isabelle-dev at in.tum.de 
>> <mailto: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 <mailto: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 <mailto: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 --------------
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/20220825/244ff4be/attachment-0001.bin>