Open work

The type-system roadmap and compiler roadmap set priorities and acceptance criteria. This backlog records remaining work, not completed milestones or benchmark results. D-numbers refer to the current decision record. Superseded decisions are kept in Git rather than in a second backlog.

Correctness first

The original signature/result-check, nested-negation, scalar-cap and rule-certainty failures are repaired; union equivalence and the common-supertype contract are corrected too. Follow-ups fix signature stability across tiers and optimization, runtime argument diagnostic differences, exact excluded-set accumulation for range proofs, and DMN wildcard/scope handling (D-219, DD-43). The open obligations separate what is in place from the broader obligations below.

• [ ] Complete the remaining R1–R8 audit and validation work before claiming general soundness. Extend the permanent counterexamples into independent constructor, variance and bound-direction checks across every proof consumer and declaration/projection path. Path and descendant readers now approximate inspected unions locally. The remaining-reader audit repairs filter binding, recursive equality, descendant shapes, context/callback images and generic flattening; its bounded independent oracle covers structural declarations and positive subtype claims. Extend this to functions, recursive names, arbitrary host contexts and the full constructor space.
• [ ] Distinguish exact sets, possible-value upper bounds and certain-input lower bounds throughout analysis. A failed subtype proof must not be treated as proof of non-inclusion.
• [ ] Validate rule witnesses against the original unary tests. Coverage, overlap and dead-rule reports need the correct approximation direction and explicit assumptions.
• [ ] Track observable errors and effects separately from returned values. A non-null or constant result type does not establish that evaluation reports no error or cannot stop in strict mode.
• [ ] Strengthen independent semantic oracles and optimized/unoptimized comparisons on both backends, including strict-mode diagnostics, composite declarations, cap boundaries and higher-order values. Keep a reproducer when a sweep finds a failure; see the sweep workflow.

Type precision and modeling

• [ ] Use the narrowing gap catalog and tagged construct-suite cases to choose precision work. Three-outcome facts and stored-condition origins already exist (D-194); extend their coverage rather than reimplementing them.
• [ ] Preserve more callable summaries across returned aliases, selections, containers and bounded alternatives (D-171, D-193, D-203). Literal signatures already stay fixed in their kind-only written environment (D-219); new call summaries must preserve that distinction and alternatives such as empty-list selection results. Summary exhaustion must lose precision safely, including in negative positions.
• [ ] Extend guarded recursive relations and independent oracle coverage (D-189). Complete finite-data membership is implemented; general recursive subtyping and equivalence are not. Exercise generated mutual graphs before broadening proof rules, and improve call precision lost through graph projection, overlapping runtime signatures and complete-callee bounds without turning call facts into signature proofs.
• [ ] Extend argument-dependent built-in result rules beyond the existing list-function rules; improve certain-mismatch reporting when only nullability or an empty range/list keeps an overload alive (D-56, D-151, D-155). Do not reject valid empty or unbounded values.
• [ ] Represent additional list cardinalities and ranges known to have endpoints before using them to prove indexing or range-call facts. Decide which refinements need public syntax.
• [ ] Complete grain propagation through parameters, paths, filters, conditionals and temporal values (D-161, D-170). Declared grain, inferred grain and runtime rounding need one explicit contract.
• [ ] Extend inverse reasoning for time/date-time arithmetic, duration failure regions and additional predicates. Exercise zones, calendar clamping, fractional seconds and representational boundaries.
• [ ] Improve correlations between repeated compound expressions and related declarations. Independent interval bounds do not keep a relation such as age <= max age when both values vary.
• [ ] Define how a component constraint of a named type refers to its containing value (D-51, D-170). A variable-specific path such as emp.limit does not solve that reusable-type problem.
• [ ] Complete supported inverse facts for boolean built-ins used directly as conditions, range-valued x in r, powers, string prefixes and case conversion (D-194). An explicit fact-table representation remains a separate refactor, not an implemented feature.
• [ ] Preserve repeated-value correlation in string addition. s + s for a string whose allowed values are "a" and "b" is "aa", "ab", "ba" or "bb", where one value gives "aa" or "bb"; the numeric one-value sums have a correlation rule (D-170, D-207). Duration self-addition also needs work: it can still combine independent intervals and admit mixed sums.
• [ ] Add month-duration scaling failure regions with the actual rounding semantics (D-204).
• [ ] Extend table-entry facts to later entries and use earlier rules' failure facts for FIRST outputs. Current narrowing uses only the matching rule's own entries (D-195).

Unresolved interpretation choices

• [ ] Decide whether declared context member names should guide parsing after . and inside filters. D-27 currently uses lexical boundaries; changing this requires an explicit parsing contract.

Declarations and language boundaries

• [ ] Preserve the meaning of composite declarations while compiling reusable membership checks. Current union/negation declarations can rebuild an analysis representation during each check (D-178); optimize only after membership correctness is established.
• [ ] Define allowed-value refinement and conversion rules for unions and negations. Host API support does not imply expression syntax for unions, intersections or arbitrary differences.
• [ ] Test the constraint of a member or an element of the result against the type the expression has for it, and not against the declared one. AllowedValues.result_member/4 gives the tests the declared member type, so {name: "M", age: 200} for a type whose age allows [0..150] gets no :unsatisfiable_allowed_values when it is prepared, whereas the scalar 200 does get it; :value_not_allowed at run time is right in both. The member type of the inferred type is Feel.Analysis.Paths.select/2 along the steps, and the elements of the lists for :each, falling back to the declared member where the inferred type is not a context or a list. The analyzer's unsatisfiable_result/5 speaks only of the result as a whole (steps: []) and says nothing about each: true, so the warning also needs a clause for a member path with its own consequence. Keep the run-time check.
• [ ] Give a member of a declared context type written as a string the key that a value has (D-213). Feel.Type.parse/2 keeps "first name" as it is, while the entry {"first name": 1} is keyed first name, so the member is not found in the value. Decide it with the same predicate.
• [ ] Resolve non-null contracts consistently: function parameter/result metadata, public type projection, and the currently rejected non-null result_type constraint (D-48). Preserve the repaired distinction between nullable runtime result signatures and precise call results, and the variance checks in public function projection, when extending this contract.
• [ ] Specify per-binding declaration policies and the assumptions exposed to callers. :trust, :audit, :report and :ignore do not establish the same facts as :enforce.
• [ ] External function definitions are :not_implemented unless an extension adds the function for their kind; feel_java does this for Java (D-211). Not done there: instance methods and constructors, other kinds (pmml, onnx), a precompiled class instead of the source a start compiles, and parallel calls (calls are serialized per sidecar).
• [ ] Treat B-FEEL semantics as separate work; the existing S-FEEL option restricts syntax. Clarify the intended S-FEEL role restrictions before adding another compatibility mode (D-49).
• [ ] Select further Camunda compatibility features from reproduced cases. Additions belong in extensions with explicit behavior, rather than silently changing core FEEL semantics (D-81).

Resource bounds

• [ ] Further reduce transfers of required large values and DMN diagnostic source metadata without relaxing validation or containment. Prepared FEEL binding projection and compact DMN dependency views are implemented; unknown metadata and uncertain spellings conservatively fall back. Compare protected public APIs separately from the trusted engine benchmark; a constant-time expression can still have input-linear cost when it consumes a large list or context.

The security model describes current limits and caller isolation. Remaining work includes:

• [ ] Reduce repeated body analysis, specialization and type expansion within the existing worker deadline and heap policy. Evaluate preparation-local memoization or optional precision caps on measured expensive shapes; exhausting optional analysis must not skip required semantic checks. No general step quota is planned.
• [ ] Earlier accounting in BEAM emission, including large constants, before allocating all generated forms. The final statement-count check happens after emission.
• [ ] Audit allocation before heap-policy checks: retained backing binaries, value copies and host calls. Per-value limits and a process heap policy do not measure all VM memory use.
• [ ] A bounded hostile-input harness for preparation and evaluation, with external timeout/heap containment and recorded inputs. Avoid running resource-exhaustion probes in the caller's process.

Performance

Measure with scripts/bench.exs; keep the command, revision, toolchain, workload and raw results with any optimization proposal. Fitted scaling exponents over a finite range are evidence, not complexity proofs.

• [ ] Investigate large generated branch chains and compiler cost in :compile.forms; compare flatter emission against current splitting before choosing a representation.
• [ ] Reduce repeated analysis of function bodies and composite declarations with preparation-local caching and bounded specialization. Do not merge analyses with different assumptions or effects.
• [ ] Profile the :full/:core seam and decide whether another analysis tier earns its maintenance cost.
• [ ] Evaluate reuse and BEAM break-even cost on representative decision workloads, not only small scalar expressions. Include preparation, module lifetime and cleanup.

Release and tooling

• [ ] Implement the currently rejected profile: :explain only with bounded traces and a defined event vocabulary. Trace the original execution so diagnostics and host calls are not replayed for explanation.
• [ ] Expand mutation coverage around algebra, caps and proof consumers; periodically run the full sweeps and both backends. A passing slice can miss a small class of counterexamples.
• [ ] Triage generated-mutation survivors: separate safely wider types from missed under-approximations, rerun flaky cases, and sample further seeds (200 of 4,107 sites are done, D-217; the twelve too-small types it left to unit tests are seen by the sweeps since D-218). Left from D-206, D-217 and D-218:
  • The survivors of the first sample (six undecided, thirty held by unit tests) cannot be run again by name: the site count moved from 2,351 to 2,612 and the names are not those of the notes.
  • Sample the analysis files outside D-217's 17 (temporal arithmetic, null reasons, iterations, filters).
  • A thin catch is noticed when it is gone, not when it thins; a floor on the count would flag it earlier (date with a year past the calendar is caught by one binding of each of two expressions).
  • The mutants job is slow on a hosted runner: 2 cores, 6 to 8 minutes a mutant at --jobs 2, so 90 to 120 minutes for 27 (the 45-minute limit cancelled it with 9 to 13 of 19 done; timeout-minutes is 150 now). A private repository has 3,000 Actions minutes a month for everything, so it is in .github/workflows/weekly.yml, weekly and on request, and not in ci.yml: a change to the sweeps or the analysis needs a manual run of it before the merge. Shards of a matrix would cut the wall time and pay for the copy unchanged in each.
  • Exercise numbers past 1E6 without multiplying every ordinary pool: the two overflow mutants are held by unit tests only.
• [ ] Keep fixture provenance, known failures and accepted flag mismatches explicit. Review changes to TCK baselines rather than accepting every change through --update.
• [ ] Document API stability before publishing. The release scope is feel and dmn (the Java packages are not released for now). No version has been released; the assessments distinguish existing behavior from the proposed target design.