potential collaborator

[Dustin Wehr]

Hey,

I think I'm interested in getting involved in either or both of the programming or foundational side. I thought I should say Hi and a bit about myself relatively early in the process of reading the docs, Hvitved's thesis, going through the tutorial, etc.

I completed my PhD two years ago in "applied theoretical computer science", to borrow Hvitved's term, with a thesis titled "Rigorous Deductive Argumentation for Socially Relevant Issues". I think it has a lot in common with Legalese, but at this date it is probably too idealistic to be of use. I'm interested in working on something more practical. 

Some things I can bring:

• Expertise in formal logic/languages, including: 
  
• A lot of experience with formalizations involving vagueness, uncertainty, and subjectiveness, on problems more applied than the toys that philosopher-logicians and CS-logicians like to work on.
• Good experience with automated and interactive theorem proving.
• Strong background in programming languages.
• General strength in CS, programming, and math.  
  
• An incorporated Canadian nonprofit, essentially the continuation of my thesis work, with an impressive board of mostly lawyers, mathematicians and computer scientists, which can receive grants from Canadian institutions. I have experience applying for some law grants, together with my cofounder (a law student with a full scholarship at a top Canadian school).
  
• Connections at the University of Toronto, McGill, Google, various other universities, various other tech giants. The bottom line being that I have some very talented and well-off friends, the latter of which give thousands to charities. 
  
• Enough savings to work for free for a while.
  
• A realtime-collaborative client-side web-based structure editor builder, which can yield an IDE for V2 or V4, for example. It uses the Google Realtime API, which powers the collaboration features of Google Docs. I designed it to be pleasant to use by both non-programmers (e.g. lawyers) and programers, including attention to aesthetics. I made it mainly to use as a kind of IDE to support the process advocated by the aforementioned nonprofit, but I made it very generic to be more widely useful. It is highly configurable, with style, allowed grammar/structures, content assist, etc all determined by a language definition, and it is easy to add significant language-specific features -- for example, integration of an automated theorem prover from TPTP server or one's own. Let me know if there's possible interest, in which case I'll pause the current refactoring I'm doing (in preparation for open sourcing) and prepare a demo build.

The areas listed in https://legalese.com/v1.0/page/contact that appeal to me most immediately are:

• Formal Methods
  
• Design and Implementation of Domain Specific Languages
  
• Fintech/Blockchain
  
• Source-to-source translation 
  
• Natural Language Processing or Library Creation - but my interest in these areas might be naive, since I don't have a background in law.

I would love to see the current work on V2 and V4.

Thanks for hearing me out,

Dustin Wehr

(note: poorly curated web presence, but my linkedin profile is ok)

[drlawrencelau]

Some some random thoughts ... one of the assumptions behind contracts is that it is usually 1-1, between just two parties. However, with social collaboration, why not multi-party? Traditionally the reasons against multi-party contracts are:

a) legal caselaw developed from bargaining theory and failures thereof

b) communications costs of coordination ... cost goes up as square of participants

c) never really been any real use-case ... most variants can be handled as side contracts, deeds or novation

It seems to me that if you've got the tools for multi-collaborative editing ... ever thought about what crowd-sourced laws (eg social compacts) might look like?

Lawrence

http://www.linkedin.com/in/drllau

[Wong Meng Weng]

greetings! Thanks for writing! I'm making my way through your PhD thesis but already I can see good overlap.

You mentioned Hvitved's PhD thesis – that's got a great survey chapter.

I'd also like to recommend John Camilleri's thesis, https://gupea.ub.gu.se/bitstream/2077/40725/1/gupea_2077_40725_1.pdf

which shows some applications in model checking, (controlled) natural language translation, and graphical visualization.

I've been working through that thesis, getting up to speed with the relevant underlying technologies like Uppaal in particular and SAT/SMT generally. (My first exposure to model checking was with Alloy.)

My current plan is to adapt the CL body of work to run on top of the CSL formalism, and sketch up some draft clauses and contracts that will GF to English and at least one other language.

How's your French?

--
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+unsubscribe@lists.legalese.com.
To post to this group, send email to ta...@lists.legalese.com.

--

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]

Hey Lawrence,

The multi-collaborative editing functionality is just a consequence of the particular solution I chose for two-party simultaneous editing (Google's implementation of an "operational transforms" library). The main reason I implemented collaborative editing was to avoid subjecting non-programmer users to the barrier of version control. I think the option of locks on documents and sections of documents is important too. But branching and merging? If it's frustrating sometimes for me, then it's too frustrating for non-programmers, who, having collaborated in groups successfully enough throughout their career, won't be convinced of the value, leaving us looking out of touch.

As far as crowd-sourced authoring of laws; no, I haven't given it much thought, though I certainly think it's worthy of it. I have thought about crowd-sourced correction of defects in judicial decisions and laws, as a more modest goal... though obviously still quite utopian. When pressed for a possible application of my thesis work, I sometimes put forward this: 

Whenever the state convicts someone of a serious criminal offence, they must commit to a high-level "interpreted formal proof" (defined in my thesis; basically just a predicate logic proof with prosed attached to each fundamental symbol, giving its intended semantics) of the person's guilt, where the axioms used in the proof must be falsifiable but need not be well-justified at the time of conviction -- it is still the job of the jury or judge to decide if the axioms are well-justified. However, if, in the future, one of the axioms is convincingly (to a judge) refuted by new evidence, a new trial is automatically awarded; the prosecution has no opportunity to backpedal on the importance of that axiom for their case of guilt. I believe such a system, if implemented well, would have expedited every case of wrongful conviction that I've ever looked closely at, as well as led to the overturning of many bad convictions that still remain, despite intense effort by advocates. 

Thanks for writing! 

Dustin

[Dustin Wehr]

Hi Meng,

I think SMT is the way to go as well. I recently used a solver to complete an argument from my thesis that I stopped short of fully formally verifying. At the time, I was only using first-order theorem provers and manual proof construction. In the process I used the SMT solver to find some minor deficiencies / missing axioms in my original partial formal proof. It was all very fast once I got the translation right (specifically, to CVC4's theory of finite sets). Performance by general first order theorem provers on finding counter models and proofs from large sets of axioms, from my experience so far, seems to be too unreliable to depend on. I assume it's even worse in HOLs. 

I'll have your current plan in mind as I read more of those two theses. I'm afraid my French is basically nonexistent (born in Canada, grew up in Ohio), though my partner, the cofounder of my fledgling nonprofit, is fluent. 

Happy to hear from you! 

Dustin

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.