Systematic, Ontological, Undiscovered Fact Finding Logic Engine | Hacker News Reader

Systematic, Ontological, Undiscovered Fact Finding Logic Engine

souffle-lang.github.io

57 pointsxrayarx7 comments

From the site:

Soufflé provides the ability to rapid prototype and make deep design space explorations possible. A wide range of applications have been implemented in the Soufflé language, e.g., static program analysis for Java DOOP, parallelizing compiler framework Insieme, binary disassembler DDISASM, security analysis for cloud computing, and security analysis for smart contracts Gigahorse, Securify, Secuify V2.0, VANDAL.

I wonder who might be able to make use of this.

Here is the license, from their LICENSE file on Github:

>The Universal Permissive License (UPL), Version 1.0

Does anyone have a use-case for a programming language like this? I am finding it hard to visualize what it does.

It is a deterministic, explicit Artificial Intelligence, where you define entities and their relations and can query about the states of facts.

The use-case may involve exploration (automated deduction) of a defined world. It is an automated Analyst. (Input an Economy, ask about some recession; input a war, ask about some battle etc.)

In the real, real world, the use case should broadly overlap with that of Prolog.

Ahhh, imagine an enterprise scale cloud of AWS service modules networked together for a security obsessed client with multiple customer access levels [1]

Then build a tool that crawls the AWS descriptions and spits out a "pure logic" description of nodes and properties [2], a graph of the network with property attributes.

The claim here is that:

> TIROS encodes the semantics of AWS networking concepts into logic and then uses a variety of reasoning engines to verify security-related properties.

> Tools that TIROS can use include SOUFFLÉ [17], MONOSAT [3], and VAMPIRE [23].

> TIROS performs its analysis statically: it sends no packets on the customer’s network.

> This distinction is important. The size of many customer networks makes it intractable to find problems through traditional network probing or penetration testing.

> TIROS allows users to gain assurance about the security of their networks that would be impossible through testing.

In other words the use-cases are static analyis of big complex intertwined balls of string, compiler trees, networked nodes, etc.

( Souffle creator | maintainer talk here [3] - I've only just started watching this, may be of interest )

[1] https://www.youtube.com/watch?v=gJhV35-QBE8

[2] https://link.springer.com/chapter/10.1007/978-3-030-25543-5_...

[3] https://www.youtube.com/watch?v=Qp3zfM-JSx8

Another view of Datalog, the underlying language, is a graph database with nodes of one verb and an arbitrary amount of objects/subjects. The query language only allows fixed verbs, but it has a built-in reasoning engine that lets you deduce new graph nodes from querying existing subgraphs.

It was/is used to prototype Rust’s borrow checking rules, which are part of a really complex type system

I heard rust author Niko mention it in a talk a few years ago, and it’s mentioned here too http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-a...

Reply on news.ycombinator.com