Skip to content

Section 18: Minimum Viable Prototype and Implementation Scope

TECHSPEC-18 — Section 18 · Version 0.1 · Status: Initial Draft

Status: draft. This section is an Initial Draft (Section 57 is a Working Register). It describes intended or proposed behavior, not a finalized, implemented language rule. Do not treat examples here as normative.

1. Prototype Philosophy

The first implementation must prove the language's central idea:

A program should be checked against its declared requirements before it is accepted as valid.

The prototype must be a working compiler, not a mockup, syntax demonstration, or collection of disconnected features.

The initial implementation should prioritize correctness, clear diagnostics, and honest verification reporting over feature count.

2. Initial Compilation Target

The first compilation target will be Python.

Rules: - The language must have its own syntax and semantics. - Python must serve only as the initial execution target. - Python's implicit behavior must not define the source language's rules. - The compiler must validate source code before generating Python. - Generated Python must not bypass guarantees enforced by the source compiler. - Future compilation targets may include WebAssembly and native machine code.

3. Required Language Features

The first prototype must support:

  • Module declarations.
  • Imports.
  • Public and private declarations.
  • Explicit variable types.
  • Immutable and mutable variables.
  • Primitive types.
  • Structs and enums.
  • Function declarations.
  • Explicit return types.
  • Conditional statements.
  • Basic loops.
  • Preconditions.
  • Postconditions.
  • Object invariants.
  • Basic effect declarations.
  • Typed Result values.
  • Explicit error handling.

Advanced ownership, borrowing, and concurrency features may be deferred until their rules can be implemented and tested reliably.

4. Required Compiler Components

The initial compiler must include:

  1. Lexer: Converts source text into tokens.
  2. Parser: Converts tokens into a structured syntax tree.
  3. Semantic Analyzer: Checks declarations, scopes, and language rules.
  4. Type Checker: Validates types and function signatures.
  5. Contract Checker: Checks contracts where supported.
  6. Effect Analyzer: Tracks declared and inferred effects.
  7. Diagnostic Generator: Produces structured compiler errors.
  8. Intermediate Representation: Provides a controlled representation between source analysis and code generation.
  9. Python Code Generator: Produces executable Python from accepted source code.
  10. Verification Reporter: Records what was checked, tested, proven, failed, or left unknown.

5. Initial Verification Capabilities

The prototype must support:

  • Static type checking.
  • Variable initialization checks.
  • Immutable reassignment detection.
  • Function signature validation.
  • Basic contract checks.
  • Runtime precondition and postcondition checks where static verification is insufficient.
  • Object invariant checks.
  • Explicit Result handling.
  • Basic effect declaration checks.
  • Unit tests.
  • Boundary tests.
  • Structured verification reports.

The compiler must not claim that a property is proven when it has only been tested or checked at runtime.

6. Initial Demonstration Program

The first demonstration program will be a Bank Account system.

It must demonstrate: - Account creation. - Depositing funds. - Withdrawing funds. - Balance retrieval. - Invalid transaction rejection. - Insufficient funds handling. - Balance invariants. - Function contracts. - Explicit error handling.

The compiler must reject implementations that violate enforceable language rules or required contracts.

Tests must demonstrate both accepted and rejected implementations.

7. Explicitly Deferred Features

The following features are outside the initial prototype scope:

  • Native machine-code compilation.
  • Advanced formal theorem proving.
  • General-purpose termination proofs.
  • Complex concurrency.
  • Distributed computing.
  • Advanced ownership and borrowing analysis.
  • Package registry.
  • Full networking and database libraries.
  • Automated AI debugging.
  • Advanced security analysis.
  • Complete standard library.

These features may be introduced after the core compiler is working reliably.

8. Prototype Acceptance Criteria

The prototype is considered functionally complete only when:

  • Valid source programs compile successfully.
  • Invalid types are rejected.
  • Invalid declarations are rejected.
  • Uninitialized variables are detected.
  • Immutable reassignment is rejected.
  • Invalid function contracts are detected where supported.
  • Runtime contract violations are reported.
  • Unhandled Results are rejected.
  • Required tests execute and report their actual outcomes.
  • Failed mandatory checks prevent acceptance.
  • Verification reports distinguish PROVEN, TESTED, CHECKED, FAILED, and UNKNOWN.
  • Generated Python corresponds to the accepted source program.
  • The compiler can explain why rejected programs failed.

A feature must not be marked complete merely because its syntax parses or its example compiles.

9. Implementation Order

The prototype should be developed in this order:

  1. Define the initial language grammar and semantics.
  2. Implement lexical analysis and parsing.
  3. Implement declarations, scopes, and type checking.
  4. Implement functions and control flow.
  5. Implement contracts and runtime checks.
  6. Implement typed failures and Result handling.
  7. Implement effect checking.
  8. Implement Python code generation.
  9. Implement automated tests.
  10. Implement verification reports.
  11. Validate the Bank Account demonstration.
  12. Document known limitations.

Each stage must be tested before the next stage is treated as complete.

10. Design Goal

The first prototype must establish that correctness-oriented language rules can be enforced by a real compiler.

A small language that reliably rejects known invalid programs is more valuable than a large language that merely makes unreliable code easier to generate.

The prototype's success must be measured by what it demonstrably catches and verifies, not by the number of features it advertises.


Source file: TECHSPEC-18.md (preserved in source-original/LANG/). See the specification index, the glossary, and the cross-reference index.