Verity Language Specification

Introduction

This document defines the Verity programming language by placing requirements on surrounding tooling. Any program claiming to be a compiler for Verity must conform to the requirements found in this document; non-compliant compilers are buggy by definition. This document will also place requirements on tooling other than compilers. This includes LSP implementations, IDEs, linters, documentation generators, etc.

Before diving into requirements, in order to more clearly portray an informal understanding of the Verity programming language, this first section describes what to expect through goals and design principles. These are also vital to keep in mind as a kind of north star when designing future revisions to this specification, extensions to the Verity programming language, or other tooling. Consistency is key in programming language ecosystems and this first section defines that consistency. Note that this section takes a much more informal tone than the rest of the document.

The remainder of this document establishes a quasi-formal definition about what does and does not qualify as a Verity program, compiler, tool, etc. These rules are prescriptive and authoritative. They are meant primarily to be read by authors of Verity tooling seeking to conform to the edge cases of the Verity language, but they should be accessible to the particularly savvy Verity user as well.

Purpose of Verity

Verity exists to close the gap as much as possible between doing engineering and writing code. Why? Design docs age and get stale. Documentation and comments get passed over on updates. TODOs sit forever without being tracked in a work queue. Assumptions and contracts are made and ignored. But code never lies. Everything listed above was real engineering, and should be streamlined by engineering tools such as programming languages.

This leads to the defining trait of Verity's design decisions. Every decision in Verity is made first and foremost to maximize the expressive power of the language, enabling the user to write their intent directly into code and enabling the compiler to aid in achieving it. When a decision must be made between two opposing views, the guiding question is what is most expressive (and it often leads to a third, better solution).

A few important properties flow directly from this (in no particular order):

• Contract-based programming is simply the expression of preconditions and postconditions, and compiler aid thereof is formal verification.
• Robust metaprogramming and reflection systems are required for users to express higher-order ideas.
• Low-level pointer arithmetic, memory management, and atomic operations must be available to express highly optimized algorithms.
• Ideas expressed by users must remain stable regardless of how the code or context changes.

Design Principles

Further flowing from the above, several design principles emerge (in no particular order):

• Language features track human intuition and ideas; code is one-to-one exposition of algorithms.
• Verity is fully extensible; every language built-in can in principle be built with the tools Verity provides.
• Every feature is fluid; no bifurcation of language rules or strict coloring of entities.
• Code is fully generic by default; specialization is opt-in.
• Don't make trade-offs for the user; give the user the tools to make their own trade-offs.
• Formal verification enables advanced expressiveness features in surprising ways.
• Validity (whether or not the program compiles), as a property of the program, is predictable, deterministic, and local.
• Versioning should be explicit and universal; portability is default and dependencies are opt-in.

Even beyond those, the following principles are important to secondary concerns for programming languages seeking broad appeal (in no particular order):

• The principle of least surprise suggests a procedural language with C-like syntax.
• An extensive standard library and a cohesive third-party module import system.
• C FFI support is non-negotiable.
• Usability across nationalities with differing (natural) languages, character sets and keyboard layouts.

Basic Definitions and Concepts

Analysis and Behavior

Some but not all tools have additional requirements of whole program analysis. These requirements apply to compilers, interpreters, LSP implementations, and IDEs as well as any other tool which performs semantic analysis at the project level.

The wording of this document is phrased primarily in terms of a valid Verity program (described below) and its behavior. Since this document primarily places obligations on tooling, the requirements in general are:

• When presented with a valid Verity program, a conforming tool must accept the program without error and reflect the behavior of the program it describes.
  • In the case of a compiler, this means emitting a binary that precisely emulates the observable behavior of that program.
  • In the case of an interpreter, this means behaving in a manner that precisely emulates the observable behavior of that program.
  • In the case of source code navigation/analysis tools, this means that the source code is broken into the lexical/grammatical structure described by this document, and any semantics reflected by the tool is consistent with the semantics of the program as described by this document.
• When presented with an invalid Verity program, a conforming tool must process the program without error and emit messages to the user as appropriate.
  • In the case of a tool for which whole program analysis is required, this means that at least one error level (or higher) diagnostic message is emitted to the user.
  • In the case of a compiler, this additionally means that no binary is generated.
• If something is required for a valid Verity program, conforming implementations for which whole program analysis is required must confirm that the requirement is met.
• If something is explicitly NOT required for a valid Verity program, conforming implementations must operate successfully with or without that property.
• If a Verity program has undefined behavior, no requirements are placed on the implementation regarding the behavior of the program.

The above behavior should not be confused with verbage hooking into Verity's formal verification system:

• When a feature enforces a condition, that condition is a proof obligation at the lexical point immediately prior to where the enforcing feature is invoked.
• When a feature guarantees a condition, that can be used as a known from the lexical point immediately after the guaranteeing feature is invoked. A guarantee must also be true in the resulting binary provided that the enforced preconditions are met.

The specifications in this document intentionally require conforming implementations to reject programs which do not meet the requirements of a valid Verity program. Implementations are NOT permitted to extend the language by accepting otherwise invalid Verity programs. Extensions must be done via an extension version (see below). This makes it possible to write a Verity program on one conforming implementation of Verity and have reasonable expectation that it will compile and behave identically on all conforming implementations.

Verity Programs

A Verity program is a collection of source code files.

• The files are organized into a hierarchical directory structure.
• Each source file must be a regular text file of finite size.
• Each source file must be readable by the tool.
• It is recommended that Verity source files be recognized under the file extension *.vty, but this extension is not required for a valid Verity file.
• Some features of Verity reference other files by string path.
  • These paths use . and .. to refer to the present and parent directories respectively.
  • These paths use / as the path separator.
  • These paths are never absolute, and unless otherwise specified are relative to the directory containing the source file where the path is used.
• Verity defines a script file build.vty at the root of a project.
• This script is not required for a valid verity project.
• It is recommended that tools provide default behavior when this script is present.
• If present, this script can be run to build the entire Verity project.
• The manner in which the tool determines the root project directory for finding build.vty or discovers Verity source files in its absence is implementation defined.

Diagnostics

Some tools may emit diagnostic messages to users. When doing so, diagnostics must satisfy the following:

• Every diagnostic message has an associated level, which exists on a continuum from low to high.
• At least one diagnostic level is emitted only for invalid Verity programs.
  • The lowest such level is referred to in this document as error.
  • All diagnostic levels higher than error are also emitted only for invalid Verity programs.
  • For tools performing whole program analysis, at least one diagnostic at error level or higher is emitted for any invalid Verity program.
  • In tools that work with multiple languages, error level diagnostics should map to traditional errors.
• At least one diagnostic level (warning) exists below error level.
  • In tools that work with multiple languages, warning level diagnostics should map to traditional warnings.
• Exactly one diagnostic level (danger) lies in between error and warning level.
  • While a conforming compiler will emit a binary when only danger level (and lower) diagnostics are emitted, tools must make every effort to deliver a danger level diagnostic to the user.
  • Precisely, tools must offer no means of hiding danger level diagnostics not also available to error level diagnostics.
  • In particular, compilers must not offer any means of suppressing danger level diagnostics.
  • The purpose of the danger diagnostic is to strongly deter against usage of unsafe language features capable of introducing undefined behavior.

Additionally, it should be noted that this document defines diagnostics such that the following hold. Any extension versions must have these properties as well:

• A program which compiles without danger (or higher) level diagnostics has fully defined behavior.
• This implies that a program which does not emit danger level diagnostics (even if it emits higher or lower levels) cannot be run without fully defined behavior.
• The entire core and standard library compiles without any danger level diagnostics.

Versions

Both this document and Verity source code are versioned using SemVer. Verity defines a breaking change (suitable for bumping a major version) as occurring when a valid Verity program in one version becomes invalid or has altered behavior in a subsequent version after changing only the version declaration in the source. But even when a breaking change is performed, Verity tools are required to remain backwards compatible via version declarations. Tools must interpret the version of each source file independently as follows:

• When a file has a version declaration specifying major, minor, and patch values, the tool must use exactly that version of the standard to interpret the file.
• When a file has a version declaration specifying major and minor values only, the tool must use the latest patch value available to that tool and compatible with the declared major and minor values.
• When a file has a version declaration specifying major value only, the tool must use the latest minor and patch values available to that tool and compatible with the declared major value.
• When a file has no version declaration, the tool must use the latest standard version of Verity available to it.
• When a file has a version declaration specifying a non-standard version (outside of the SemVer system), the tool may interpret that version in an implementation-defined manner, including as an extension to the Verity programming language.
• When a file has a version declaration specifying a version which the tool does not support, the tool must emit at least one error (or higher) level diagnostic.