___________                         .__   
\_   _____/__________  _____ _____  |  |   
 |    __)/  _ \_  __ \/     \\__  \ |  |   
 |     \(  <_> )  | \/  Y Y  \/ __ \|  |__ 
 \___  / \____/|__|  |__|_|  (____  /____/
     \/                    \/     \/          

Towards an embedded domain-specific language (DSL) for verifiable vector-calculus computations.

Formal supports research on mimetic software abstractions for vector calculus by providing

• Derived types that mimic vector and tensor fields and
• Differential and integral operators for writing vector and tensor expressions.

Formal's types and operators implement the discrete calculus of Corbino & Castillo (2020) and Dumett & Castillo (2022): mimetic numerical methods that satisfy discrete versions of vector calculus theorems.

Mimetic software abstractions use mimetic numerical methods to mimic desirable behaviors of the abstractions' vector calculus counterparts. For example, given scalar and vector fields $f$ and $\vec{v}$ defined over a unit volume $V = [0,1]^3$ bounded by a surface area $A$, the program example/extended-gauss-divergence.F90 demonstrates satisfaction of the extended Gauss divergence theorem:

$$ \iiint_V (\vec{v} \cdot \nabla f) dV + \iiint_V (f \nabla \cdot \vec{v}) dV = \iint_A f \vec{v} \cdot d\vec{A} $$

which ensures the satisfaction conservation laws such as those for mass, momentum, and energy.

Running the program as follows

fpm run --example extended-gauss-divergence --compiler flang --profile release

produces output that includes actual program syntax:

    f = (x**2)/2 ! <-- scalar function
    v = x        ! <-- vector function
.SSS. (v .dot. .grad. f) * dV =  .3333333330205934
.SSS. (     f * .div. v) * dV =  .16666666739857125
   -.SS. (f .x. (v .dot. dA)) = -.5000000004191649
----------------------------------------------------
                          sum = -.2220446049250313E-15 (residual)

where the small residual evidences a highly accurate approximation.

Future work: Formal lays a foundation for defining a verifiable embedded DSL using type-safe generic programming.

Formal now supports 2D and 3D operators that compute the gradient (.grad.) of a scalar field, the divergence (.div.) of a vector field, and the arithmetic operators required for expressing equations such as the advection/diffusion partial differential equation (PDE):

$$ \partial s / \partial t = \nabla \cdot (D \nabla s) - \nabla \cdot (\vec{v}s)$$

which Formal facilitates writing as

ds_dt = .div. (D * .grad. s) - .div. (v * s)

where s is the concentration of a passive scalar quantity, D is a molecular diffusion coefficient, and v is a prescribed velocity field. This repository's 2D-advection-diffusion program, for example, demonstrates how to advance the above equation in time using a Runge-Kutta scheme.

See this repository's example subdirectory for additional demonstrations of using Formal. For each example, obtain usage information f execute something like

fpm run --example <base-name> -- --help

replacing <base-name> with the portion of an example file name preceding the .F90 or .f90 extension. To save typing in a terminal window, set the example directory as your present working directory before typing fpm run above. Then use tab completion to enter a file name and delete the file extension before pressing return or enter.

Building and testing Formal requires the Fortran Package Manager (fpm), which can be obtained via a package manager (e.g., brew install fpm on macOS) or by compiling the single-file concatenation of the fpm source that is included among the release assets. For the fpm 0.13.0 release, for example, compiling fpm-0.13.0.F90 and placing the resulting executable file in your PATH suffices.

With fpm Versions before 0.13.0, replace flang with flang-new and delete --profile release in the tabulated commands above.

Building with nagfor requires an fpm version containing commit 9a4433d, which was merged into fpm's main branch on 27 August 2026.

Recent commits exposed issues with the Intel ifx and gfortran compilers that block building Formal. Once the issues have been addressed, the corresponding compiler's content will be moved back up to Supported Compilers table.

The doc/uml folder contains Mermaid scripts that generate Unified Modeling Language (UML) class diagrams depicting many Formal derived types and their interrelationships. GitHub's web servers render the diagram graphically when viewed in a web browser.

Please see LICENSE.txt for the copyright and license under which Formal is distributed. To report any difficulty with building, testing, or using Formal, please submit an issue. To contribute code, please submit a pull request from a fork of Formal.

Formal is a software artifact of research funded by the Competitive Portfolios for Advanced Scientific Computing Research Program of the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research under contract DE-AC02-05CH11231.