what's the best writing on contracts? what are the best systems to study, what is the state of the art? is the clojure thing any better than anything else?
Conversation
I'm working on an essay about this right now, actually. Short of it is that there isn't a whole lot of writing outside of early Eiffel euphoria, which is unfortunate. But clojure isn't close to the cutting edge.
4
7
Those designed for static verification or those designed for runtime testing? They intersect, but they’re also somewhat distinct.
1
1
I'm trying to write about both. I'm also trying to focus on languages which include contracts as part of the language syntax, with the exception of racket and clojure (which laugh at the concept of language syntax)
2
1
The historian in me wants to point you at the Euclid family (1977 -- year I was born!) which had pre/post/invariant/assert Hoare logic constructs intended for both, _and_ prohibited mutable aliasing. As usual with Lampson, way ahead of its time :)
hopl.info/showlanguage.p
1
3
Also influential as verification-oriented / Hoare-logic-y things in that timeframe: Alphard (hopl.info/showlanguage.p), Gypsy (hopl.info/showlanguage.p).
1
1
Modern-day, I'd make sure you at least mention FStar. I think it's kinda cutting edge in the "Hoare logic discharged by SMT" family. There's some interesting stuff around predicate transformer semantics in there, so-called Dijkstra Monads.
1
5
I thought FStar was more a dependently typed thingy?
2
1
It is both. As with many dependent typed systems, it uses dependent types to encode a Hoare-logic-like weakest-precondition system for a set of its terms that model imperative/stateful code (monadically, in FStar's case). Then sends those to z3.
1
5
Really excited about more languages blurring the lines between contracts and dependent types. Not everything has to be done using manual proofs or tactics - lots can be automated.
Personal opinion: FStar is in fact pretty rad.
(As is Lean)
6