3 ms·

Systematic, Ontological, Undiscovered Fact Finding Logic Engine

57 points by xrayarx 4y ago

xrayarx 4y ago
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.
trehans 4y ago
Does anyone have a use-case for a programming language like this? I am finding it hard to visualize what it does.
- mdp2021 4y ago
  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.
- defrost 4y ago
  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 https://www.youtube.com/watch?v=gJhV35-QBE8 [2] https://link.springer.com/chapter/10.1007/978-3-030-25543-5_14 https://link.springer.com/chapter/10.1007/978-3-030-25543-5_... [3] https://www.youtube.com/watch?v=Qp3zfM-JSx8 https://www.youtube.com/watch?v=Qp3zfM-JSx8
- maweki 4y ago
  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.
- deleted 4y ago
  [deleted]
- chubot 4y ago
  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-alias-based-formulation-of-the-borrow-checker/ http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-a...
unixhero 4y ago
I wonder who might be able to make use of this. Here is the license, from their LICENSE file on Github: >Copyright (c) 2016 Oracle and/or its affiliates. All Rights reserved >The Universal Permissive License (UPL), Version 1.0

57 points by xrayarx 4y ago

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.

trehans 4y ago

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

mdp2021 4y ago
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.
defrost 4y ago
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 https://www.youtube.com/watch?v=gJhV35-QBE8 [2] https://link.springer.com/chapter/10.1007/978-3-030-25543-5_14 https://link.springer.com/chapter/10.1007/978-3-030-25543-5_... [3] https://www.youtube.com/watch?v=Qp3zfM-JSx8 https://www.youtube.com/watch?v=Qp3zfM-JSx8
maweki 4y ago
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.
deleted 4y ago
[deleted]
chubot 4y ago
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-alias-based-formulation-of-the-borrow-checker/ http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-a...

unixhero 4y ago

I wonder who might be able to make use of this. Here is the license, from their LICENSE file on Github: >Copyright (c) 2016 Oracle and/or its affiliates. All Rights reserved >The Universal Permissive License (UPL), Version 1.0