Hacker News new | ask | show | jobs
by trehans 1288 days ago
Does anyone have a use-case for a programming language like this? I am finding it hard to visualize what it does.
4 comments

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

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.

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...