Soda

Soda (Symbolic Objective Descriptive Analysis) is a functional language with object-oriented notation to describe, analyze, and model human-centered problems, especially ethical problems.

This project includes a translator (or transpiler) to Scala 3, experimental translators to Lean 4 and Coq 8, and a LaTeX documentation extraction tool.

Publications

• Julian Alfredo Mendez. Soda: An Object-Oriented Functional Language for Specifying Human-Centered Problems. arXiv   DOI:10.48550/arXiv.2310.01961   Abstract   BibTeX   PDF   Implementation

Online manual

• User manual

Where to start

Steps to run a “Hello world!” example in Soda:

1. To run these steps, you need to install:
   • a. Scala 3
   • b. sbt (if you need to build the binaries)
   • c. Java (to execute JAR files)
2. Get the translator binary by either doing the following:
   • a. download the Linux binary from releases
   • b. or clone the GitHub repository and compile it, by either:
     • i. run the makeall.sh, from a Linux compatible environment
     • ii. or run sbt to get an executable JAR file as indicated in the release notes. The command itself is described in build and the file is release. To execute a JAR file, you need a Java environment installed, and you need to run java -jar filename.jar, for a JAR file named filename.jar.
3. Once you got the binary translator, go to an empty directory and try soda manual. It will output a piece of code with many examples, but most importantly, this mini-manual is a “Hello, World!” program itself. Write soda manual > Manual.soda and you get the manual.
4. Once Manual.soda has been created, run soda .. This will create two files: Package.soda and Package.scala.
5. Run scalac Package.scala, which will compile sources and put the result in the directory soda/manual.
6. Run scala soda.manual.EntryPoint, which will show you Hello world!.

How to learn Soda

Soda is a functional language intended to be easy to learn and to read. However, writing purely functional style requires some practice, as some things are different from the imperative style. In addition, Soda includes an object-oriented notation to align it with mainstream object-oriented programming languages, and to make its notation familiar to users acquainted to those languages.

The first step is to get familiar with the functional notation and functional approach to algorithms. This can be learned by rewriting imperative pieces of code, and use Scala, which allows both paradigms, to check that both approaches give similar results.

The next step is to get familiar with classes and packages. Modeling simple examples can give a good basis to see what possibilities and limitations has to model with Soda. You will find that modeling will seem faster and easier, but you will find some limitations when modeling constrained instances. It is also a good practice to get acquainted to the syntax and naming conventions, which are useful when creating larger projects.

The next step is to get familiar with the testing possibilities. At the moment, this is only developed for the Scala translator. Some examples can be found in module examples, in the Soda repository. They can be run with sbt test.

The last step is to get familiar with the verification possibilities. For this, it would probably work better to write Lean 4 proofs, as the Soda translator to Lean is more developed than the translator to Coq. A good way to start proving theorems in Lean is to follow the tutorials at the Lean Game Server, like the Natural Number Game.

Technical details

Reserved Words and Symbols

The reserved words are:

• : (type membership symbol)
• -> (type mapping symbol)
• = (definition symbol)
• := (parameter definition symbol)
• lambda, any (synonym of lambda), --> (lambda symbol)
• if, then, else
• match, case, ==> (implication symbol in pattern matching)
• class, extends, abstract, end
• this, subtype, supertype
• false, true , not, and, or
• package, import
• directive

In addition, the language has:

• ( and ) (parentheses) for parameters and operator precedence
• [ and ] (square brackets) for parametric types

The main arithmetic operators are:

• +, -, *, /, % (modulus)

Comments are marked with /* and */. Scaladoc / Javadoc markers are /** and */.

The annotations (only available when translating to Scala) are:

• @new to create JVM instances in translations to Scala 2
• @tailrec to ensure a tail recursion
• @override to override a JVM function

The following are special names:

• _tailrec_ as prefix indicates that the function is tail recursive
• _rec_ as prefix indicates that the function is recursive
• Main is the entry point class, and Main_ () its constructor

Integration

This language is statically typed. It is possible to define abstract and concrete classes. Each class (like a trait in Scala) can be extended and has a single class constructor. This constructor is implemented with a concrete class (like a case class in Scala).

Soda is designed to be integrated via the Java Virtual Machine. It is possible to define packages and to declare imports. This can be done in a separate file Package.soda, which is in the same directory as the source code.

In Soda, variables cannot change their value. Thus, it is not possible to write x = x + 1. Loops can be managed with range and fold functions and tail recursion. The language does not provide throw, try, and catch, because those commands do not follow the functional style. Nevertheless, it is possible to produce side effects, like using files, through packages provided by Scala.

The following tools can be configured to have syntax highlighting:

• IntelliJ configuration
• gedit configuration

Build

The project can be built with sbt with sbt clean compile test package assembly

A Linux binary can be created with the script makeall.sh.

More detailed information can be found in the release notes.

Author

Julian Alfredo Mendez