Clojurians Log v2

I think generative testing can play a similar role instead of using symbolic execution. You have a static type (optimistic) and a schema (pessimistic) for each function, and the static type checker assumes the optimistic invariants, and generative testing based on the pessimistic schema raises confidence that the optimistic type is actually realistic.

All happening at dev time, so there's no overhead.

concretely:

(ann moving-average [(Seqable Num) (DefaultTyped :optimistic PosInt :pessimistic Int) :-> Num)

;; generates: 
(ann moving-average [(Seqable Num) PosInt :-> Num)
;; and
(m/=> moving-average [:=> [:seqable :number] :number :number])

Could even make this malli-specific if you're using it in prod to check schemas, using environment variables to decide whether you're in dev (pessimistic, slower) or prod (optimistic, faster).

In all cases, we'd want to assert that pessimistic <: optimistic.

Malli specific:

(m/=> moving-average [:=> [:seqable :number] [::default-typed pos-int? :number] :number])
(def default-typed-schema (m/proxy-schema (if *dev* ...))

Maybe I'm just saying this because Rosette is not targetted at Clojure 🙂

yeah I don't think I quite grok the tradeoffs of its approach vs more traditional / established ones like you mentioned, (this is mostly going off my impressions of the talk) - I didn't quite understand either why they had to bring in the Rosette / constraint solver machinery for this, from what I understand it's functioning sort of like a HM type inferencer on the program body so you don't have to go and manually annotate the rank of each sub expression?

I guess you need SMT because it's dealing with integer domain max/min and inequalities rather than plain unification.. It'd be interesting to find out how many levels of 'plausibility ranking' one actually needs in practice, the paper only presents the example with 0happy path , 1unlikely... 2~error , which you could reformulate as optimistic / pessimistic enum

..maybe something like a safety-critical system with code-green-yellow-orange-red levels of severity? But they'd probably be using formal typed systems from the start