[bug#70567] [PATCH 0/7] frama-c: Update to 28.1.

[Jean-Pierre De Jesus Diaz <jean@foundation.xyz>]

Hi,

>looking at what frama-c does, I am a bit puzzled: to me it has been put
>into the wrong module, together with why3 just above it; unless you consider
>informatics as a subset of mathematics, that is. In any case, these packages
>do not seem to do computations of interest to an applied mathematician
>(which is what most of maths.scm is about) or a pure mathematician (with
>packages in algebra.scm).

Agreed.

>Could they be moved to coq.scm? Or a more generic, maybe a new module
>related to theorem proving and/or source code analysis? Maybe into a
>renamed valgrind.scm?

I think it should be done but in a separate patch series as it would involve
moving quite a few things, maybe a formal-methods.scm module?

I think the coq.scm should be only for Coq as it contains it's own ecosystem.

On Thu, Apr 25, 2024 at 3:35 PM Andreas Enge <andreas@enge.fr> wrote:
>
> Hello,
>
> looking at what frama-c does, I am a bit puzzled: to me it has been put
> into the wrong module, together with why3 just above it; unless you consider
> informatics as a subset of mathematics, that is. In any case, these packages
> do not seem to do computations of interest to an applied mathematician
> (which is what most of maths.scm is about) or a pure mathematician (with
> packages in algebra.scm).
>
> Could they be moved to coq.scm? Or a more generic, maybe a new module
> related to theorem proving and/or source code analysis? Maybe into a
> renamed valgrind.scm?
>
> Andreas
>