Fork me on GitHub
#clojure-spec
<
2022-02-17
>
Simon16:02:56

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?

Alex Miller (Clojure team)16:02:25

what problem would this solve?

Alex Miller (Clojure team)16:02:41

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

Simon17:02:17

At a minimum something like this:

Simon17:02:08

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

Alex Miller (Clojure team)17:02:16

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

Simon17:02:22

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

Simon17:02:37

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

Simon17:02:04

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

Alex Miller (Clojure team)17:02:17

well, spec is emphatically not a type checker :)

Alex Miller (Clojure team)17:02:34

it's a predicate value system applied at runtime

Alex Miller (Clojure team)17:02:29

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

Alex Miller (Clojure team)17:02:08

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