Remove VampIR target from compiler frontend

[janmasrovira]

It was communicated by @cwgoes that we should remove the current VampIR support from the codebase.

• Related to Clean up backends and tests #2807

[lukaszcz]

We can remove the user-facing CLI commands, but we should not remove the VampIR compilation pipeline. I just realized this compilation method (after modifications) can be used to translate Juvix code to SMT constraints, enabling formal verification of program properties. We might want that in the future.

[lukaszcz]

enabling formal verification of program properties

Or rather automated bug-finding with SMT/constraint solvers: finding values of arguments for a pure Juvix function such that a given property (represented as a pure boolean Juvix function) is not satisfied.

[lukaszcz]

enabling formal verification of program properties

Or rather automated bug-finding with SMT/constraint solvers: finding values of arguments for a pure Juvix function such that a given property (represented as a pure boolean Juvix function) is not satisfied.

Or automated test-case generation by finding valuesx, y such that p(x, y) = true where p is a specification of f (p(x, y) = true iff f x = y)

In any case, I think we should keep the VampIR pipeline; we might still use it

[paulcadman]

We can remove the user-facing CLI commands, but we should not remove the VampIR compilation pipeline. I just realized this compilation method (after modifications) can be used to translate Juvix code to SMT constraints, enabling formal verification of program properties. We might want that in the future.

Understood, thanks.