Reflections on Hvitved's Chapter 2 (introducing CSL)

[Dustin Wehr]

Hvitved is a great writer, and his Chapter 2 has a few good ideas -- blame assignment, obligation vs breach distinction, assignment of a deadline to every obligation, runtime monitoring. But the vast majority of it is the formulaic fluff and trivial proofs of the CMU school of computer scientists that call themselves "type theorists". Also known as "Theory B" in complexity theory and algorithms circles. I got sucked into that mess in my last couple years as an undergrad at McGill. 

Despite being executable, which is great, I think CSL is worse overall than plain-English legal drafting. Maybe it is better overall than typical legalese. If there is interest, I can show you how I think Hvitved's examples should be written up. I think I can do it, without much trouble, in a decidable SMT theory without sacrificing readability, in which case you'll be able to pose questions that get answered instantly.

Formalized law need not look any more obscure than English + a few more parentheses + a few bound variables (which can usually be replaced with a formal analogue of pronouns).

[Dustin Wehr]

Boolean combinations of integer arithmetic inequalities and boolean variables seems to suffice, which any SMT solver will handle. 

[Dustin Wehr]

Sorry, I am overly critical and tactless. 

Anyway, I would have fun doing this as long as I know it might be appreciated, so let me know!

--
You received this message because you are subscribed to the Google Groups "Legalese talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to talk+uns...@lists.legalese.com.
To post to this group, send email to ta...@lists.legalese.com.

[Wong Meng Weng]

I would love to see how you handle his examples! Tact is irrelevant, as per http://www.mit.edu/~jcb/tact.html

I remember a CL paper that talked about Attempto. But why don't you have a go at your take on CSL first and then we can expand the scope to FormaLex and CL and then some larger real world examples.

--

colle...@legalese.com is a group email address used to provide continuity over multiple individuals.

This message was sent by meng...@legalese.com (Meng Weng Wong) on behalf of Legalese.

[Dustin Wehr]

I haven't put as much time into this as I'd have liked, but probably better to get a draft out than to wait till I can work on it more. 

The draft is written in my webapp, Structure Together, using the base "structured text" language. I have not taken the time to make a Legalese-custom language, which would improve both the reading and editing experiences. This URL sends you to a read-only view of the document, but you can change that with the button on the bottom right of the screen. Close to those are buttons that change the style from a dark theme to a light theme, and a button to show keyboard shortcuts. There's a password I'm dropping on the slack channel, just because I prefer the code not to be completely public before I open source it.

http://www.cs.toronto.edu/~wehr/st/out/scc/index.html?demo=legalese

The "Master sales agreement" and "Installment sale" examples on pages 56 and 57 of Hvitved's thesis might be worth doing too. The first would illustrate composition of contract programs (which is basically as easy as composition of finite state machines). The second would be a good test that we can reduce a bounded-time contract to SAT or SMT even when the contract has loops. 

I'd be more interested in doing a more complicated example than those, since it would present more opportunities for testing non-obvious properties, and there'd be a greater chance of getting something wrong.