A Formality Style Guide

"considering making single-line definitions with ; a syntax error to stop your kingdom of evil" --Victor Maia

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC 2119

General

Lines MUST be 80 columns or fewer in length.
names of Types MUST use camelCase
names of terms MUST use snake_case or dot.case
- snake_case SHOULD be used as the standard "word" separator
- dot.case should be used to signify inheritance or logical containment
Tabs MUST NOT be entered into files
Indentation MUST be uniform and set to 2 spaces per indent level

File Headers

All Files MUST contain a header delimited by multiline comments with following information:

An abstract description of the file's contents that begins with <file-name> contains...

For Logic.fm this looks like:

/* Logic.fm contains a variety of useful non-builtin types
 * and functions over those types
 */

Comments

Comments SHOULD be 60 columns or fewer in length
Comment sections SHOULD use the following hierarchy:

Specific Conventions

A function whose primary purpose is to convert between A : Type and B : Type SHOUlD be named A_to_B

Abstract data types and Records

Contents of an ADT must either on 1 line per variant:

T Magma {A : Type}
| magma { f : A -> A -> A }

or each variant must open a new indent level, with the brackets and commas aligned:

T Group {A : Type}
| group
  { f           : A -> A -> A
  , e           : A
  , associative : Associative(A,f)
  , identity    : Identity(A,f,e)
  , inverse     : Inverse(A,f,e,identity)
  }

The : in the type signatures must also align.