Typical Computing

Partial Verification

This feature is provisional. Its purpose and broad behavior are known, but many details of its syntax, verification model, and implementation still require clarification.

Partial Verification is the process of checking intentionally incomplete Typical code without requiring it to be a complete executable program. The system that performs this process is the Partial Verifier.

Partial Verification is intended for code embedded in documentation, intents, semantic references, and usage examples. These fragments should remain useful when their surrounding setup or irrelevant details have been omitted.

Partial Verification is not ordinary compilation. It uses the language parser, name resolution, and type system to verify the information that is present while representing omitted information explicitly.

Principles

Partial Verification may accept missing setup, omitted arguments, implied values, incomplete control flow, or other information that is unnecessary to demonstrate the point of an example. It should still discover invalid syntax, nonexistent members, impossible types, invalid visibility, unsatisfied generic constraints, and obsolete usage patterns when the supplied information is sufficient to do so.

Semantic References

Intent text may contain semantic references using substitution syntax:

(( SomeClass ))
(( Files.readFileSync ))
(( calculateThings(...) ))

Semantic references use ordinary lexical visibility and name-resolution rules. A reference that is not visible from its containing scope remains representable but produces a notice.

In the token-based editor, a resolved reference retains the stable identity of its target rather than only its textual spelling. Renaming the target updates the displayed reference. When raw text is parsed without identity information, the reference is resolved again using ordinary language rules.

Typical does not support function overloading. Functions use optional arguments, rest arguments, and sum types when they need to accept different call shapes. Consequently, (( calculateThings(...) )) does not refer to an overload family. It refers to calculateThings while deliberately omitting the details of its arguments.

Holes

The ... token may represent deliberately omitted information in a context processed by the Partial Verifier:

result = calculateThings(...)

In this example, the arguments are known to exist but are irrelevant to the example. The Partial Verifier determines whether some valid completion of the omitted argument list can satisfy the function signature.

This use of ... is contextual. Typical also uses ...value as the spread operator in ordinary code. A bare ... used as a partial hole must only be accepted in a context where Partial Verification is active.

Holes do not mean that all surrounding constraints are discarded. The Partial Verifier should infer and retain every constraint it can obtain from the enclosing expression and the referenced declaration.

A Partial Verification hole is distinct from compiler unknowable recovery. A hole deliberately stands for omitted information that may have a valid completion. Unknowable instead propagates from an operation the ordinary compiler cannot currently interpret and short-circuits its containing statement.

Implied Example Values

Usage examples often refer to values supplied by an implied surrounding environment:

result = calculateThings(request)

The value request may be an example-local input rather than a declaration that exists in the program. The Partial Verifier may infer constraints on such a value from its use.

An assumed example-local value must remain distinguishable from a misspelled or inaccessible program symbol. The editor must surface that the value has been assumed rather than silently treating every unresolved identifier as valid.

The exact syntax or editor interaction used to confirm an assumed example-local value has not been decided.

Relationship To Intent Evaluation

Partial Verification checks incomplete language fragments contained in or referenced by intents. It does not by itself determine whether a natural-language intent is true of an implementation.

Intent evaluation is a separate, continually running background process. Evaluation work is queued and processed when resources are available. That process may use the Partial Verifier when an intent contains code, a semantic reference, or an incomplete usage example.

Open Questions