FPL (Formal Proving Language)

FPL, the Formal Proving Language, is a language to formulate mathematical definitions, theorems, and proofs independently of individual natural languages.

It comes with a VS Code extension that enables you to make use of advantages of an IDE like VS Code while writing code in FPL.

Main Features

• A custom Formal Proving Language (FPL) for writing and structuring mathematical proofs independently of natural language, with rich mathematical notation and a continuously simplified, readable syntax
• A real interpreter with an execution engine capable of evaluating logical expressions and verifying proof correctness, not just parsing structure
• An extensive, fine-grained diagnostics system (100+ codes) for catching signature, syntax, and proof-justification errors
• A full-featured VS Code extension with syntax highlighting, autocompletion, symbol navigation, and a webview for browsing valid statements and rules of inference
• A Language Server Protocol implementation powering real-time diagnostics, completion, and document navigation
• Cross-platform support via on-demand .NET runtime acquisition for Windows, Linux, and macOS

Further resources

• For a more detailed feature list see RELEASE NOTES.
• For a full change log see the CHANGELOG.
• Contributions are wellcome: Read our CONTRIBUTING.md guidelines, contribute, and attribute yourself in our CONTRIBUTORS.md list.
• We also use third-party code: See THIRD_PARTY_NOTICES.md guidelines, contribute, and attribute yourself in our CONTRIBUTORS.md list.
• There is also an FPL Channel on YouTube devoted to the FPL language.

Research

This is a Proof of Concept (PoC) of a private research project to develop such a language.

• This PoC is based on the original research paper.
• See also a summary article of FPL principles.