[HN Gopher] Catala Lang: DSL designed for deriving implementatio...
___________________________________________________________________
Catala Lang: DSL designed for deriving implementations from
legislative texts
Author : wut42
Score : 45 points
Date : 2021-09-23 18:27 UTC (4 hours ago)
(HTM) web link (catala-lang.org)
(TXT) w3m dump (catala-lang.org)
| rsrsrs86 wrote:
| Working with Catala in academy. Also trying to model Catala as a
| type system embedded in Haskell
| denismerigoux wrote:
| Hi, Catala author here. This is amazing! Please get in touch if
| you have any questions or just want to talk :)
| rsrsrs86 wrote:
| How can I reach you?
| lopatin wrote:
| What are the benefits of having this be the type level? Asking
| as a reformed purist.
| rsrsrs86 wrote:
| Ok I expressed it wrong. I am just trying to embed a legal
| DSL it in Haskell and get the type system to help building
| type-safe contracts - same as embedding the STLC in GADTs
| PostThisTooFast wrote:
| DSL? In 2021?
| [deleted]
| jaytaylor wrote:
| Cool idea, I'm sure many programmers have pondered this concept
| (albeit briefly, in my case).
|
| Found a code sample in the README:
|
| https://github.com/CatalaLang/catala/raw/master/doc/images/S...
|
| Unsolicited feedback: this should be the first or second thing
| visible on the home page, ideally in a less funky font.
| spicybright wrote:
| Knee jerk reaction, I don't think a programming language will
| benefit law in any capacity.
|
| If there's a dispute around existing code, who's going to
| translate it to Catala?
|
| If there's legal reason to write a specific program for
| something, why wouldn't that be some kind of patent or similar?
|
| The only English example (US Tax Code) has a broken link too,
| "source code files of the example", so I can't even see that.
|
| Idk. Just doesn't seem useful from what I see so far.
| triska wrote:
| A healthy dose of skepticism seems certainly warranted. I would
| like to share an example that I hope illustrates the potential
| of using programming languages to formalize legal reasoning, or
| at least one possible usage scenario. Take for instance Article
| 14 of the Single Digital Gateway Regulation (SDGR), available
| in its entirety from:
|
| https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=uriserv:...
|
| Article 14 mandates that a technical system be built and
| states, among other requirements:
|
| _" Where competent authorities lawfully issue, in their own
| Member State and in an electronic format that allows automated
| exchange, evidence that is relevant for the online procedures
| referred to in paragraph 1, they shall also make such evidence
| available to requesting competent authorities from other Member
| States in an electronic format that allows automated
| exchange."_
|
| The core of this task is therefore to translate evidences
| between different European Member States. It would be nice to
| formalize this in the form of _logical rules_ that clearly
| state which documents can be used to establish the necessary
| evidences. For instance, the contents of an Austrian birth
| certificate could be used to prove a required age to a
| different Member State. The logical rules could take changes in
| legislation into account without requiring a redeployment of
| the entire system, if there is a way to read and interpret the
| rules dynamically.
| a-dub wrote:
| i found this recently and got really excited about the idea of
| computational law- but then i looked close and saw that all the
| examples were complicated tax and benefit accounting rules for
| the french government and thus rose the tombstone for my interest
| in computational law.
| triska wrote:
| Very interesting! Previous discussions:
|
| https://news.ycombinator.com/item?id=27059899 (5 months ago, 129
| comments)
|
| https://news.ycombinator.com/item?id=24948342 (10 months ago, 37
| comments)
|
| As I see it, a language intended for use in legal contexts such
| as contract law and legislation must satisfy two key desiderata:
|
| (1) it must be able to express the intended laws and contracts
|
| (2) it can used _to conveniently reason about these rules
| themselves too_.
|
| It is property (2) I miss most when seeing this proposal.
|
| When I undertake the task of formalizing legislation or any type
| of rules, one of the key benefits I would like to obtain as a
| result is the ability to answer questions such as: "Are there
| redundant regulations or clauses?", "Can these conditions be
| simplified?", "Are these conflicting conditions?" etc. Such
| questions require reasoning about these rules themselves.
| Y_Y wrote:
| I'd like to add that an ideal legal language should end up
| heavy with definitions. Whether or not a person has performed
| an action is often an important legal question, even after the
| a t is clearly defined and the person identified. To this end I
| think such a language should have some formal definitions of
| what it literally means for a specified person to perform a
| specified act.
|
| You could go on for some time defining terms here, and would
| have to if you want to mechanically determine legal outcomes,
| once the required quantifiable facts have been established. I
| think you'd end up with something look like one of the ill-
| fated expert systems of yesteryear.
| denismerigoux wrote:
| Hi, Catala author here! (2) is definitely possible since the
| language has a formalization and is proof-oriented. I have
| plans to connect it to theorem provers for the kind of
| application you're referring to, just didn't have the time to
| do it yet :)
| triska wrote:
| Thank you a lot for taking the time to respond!
|
| Could you please give a short example of how we can use
| Catala to interpret for instance the sample program that is
| shown on the project page? Does it have a natural
| representation as a Catala data structure that can be
| reasoned about conveniently within Catala?
| denismerigoux wrote:
| No, the language does not have self reflection, it is a
| domain specific language that is not even Turing complete.
| However Catala programs could be compiled to deep or
| shallow embeddings inside other programming languages,
| including inside theorem provers interactive (Coq, F*,
| Agda, etc.) or automatic (SMT solvers, abstract
| interpreters). You would then be able to reason about your
| Catala programs inside these external provers.
| breck wrote:
| I'm very interested in computational law and appreciate all links
| to people exploring this space. Another I found recently in
| Singapore: https://cclaw.smu.edu.sg/
___________________________________________________________________
(page generated 2021-09-23 23:00 UTC)