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

[Makarius]

On 26/08/2022 01:01, Achim D. Brucker wrote:

>> For example, the absorption of GHC stack and OCaml opam some years ago did
>> not fully work out: these projects have there very own culture that does not
>> fully fit into Isabelle. We did not gain the stability and
>> self-containedness of GHC and OCaml that we were hoping for: it still
>> requires manual tinkering occasionally.
> 
> I do not want to hide the truth: while dotnet/F# is a stable platform that is used in
> production, it has its own culture and tooling. The current setup only uses a tiny bit
> of it, namely "F# interactive" (the REPL, so to speak).
> 
> Without knowing exactly how much occasional manual tinkering GHC and Ocaml require, my
> best guess is that dotnet/F# would be in a similar ball park. Microsoft offers 3 years
> of support for LTS releases of dotnet. Thus, some tinkering is required every 2-3 years
> to switch to the latest LTS release. As the code generator setup maps to the (stable)
> core of the language and does not make use of any additional libraries, this should
> still fall into the "little bit of manual tinkering" category, hopefully.

Thanks. From your explanations, I have learned many things about F# and dotnet.

Can you also say what your applications are?

Dotnet was once positioned as the next big thing, but recently we have seen 
more excitement elsewhere (even by Microsoft): e.g. Node.js/Electron.


	Makarius