Clojurians Log v2

Hello Very Senior Clojure Spec question here: I’m new to Clojure-spec, but have been using Clojure for about a year now. During my thesis I implemented the compiler for Secure Guarded Commands by Flemming Nielson (my supervisor). https://link.springer.com/chapter/10.1007/978-3-030-41103-9_7 The language syntax allows the compiler to analyse the explicit, implicit, bypassing, correlation, sanitised, and indirect information flows. Such that to make sure at compile time that no information is leaked. Would it be valuable to add similar information flow analysis to Clojure Spec?

what problem would this solve?

I guess I'm wondering if you're looking to extend spec or use the information in specs to do this analysis independently?

At a minimum something like this:

I think i have some people doing something similar. https://dl.acm.org/doi/pdf/10.1145/3468264.3473127

that image makes me think you are wanting something even more fundamental, like a change to the language

not neccessarily, I think we could also use a syntax that is closer to that of spec.

it’s sort of an extension of a type checker.

and if clojure.spec checks types, then I think it would be possible to do?

well, spec is emphatically not a type checker :)

it's a predicate value system applied at runtime

some people have explored using it for static checks (https://github.com/arohner/spectrum and some work with https://github.com/clojure/core.typed)

but that's certainly not the conception or use of it in core