R9: Never goes wrong: M7a–c on M7Fragment (the empty host table, answer-free tapes)req:R9
- Open, waits on a ruling (decisions row 117: the frame contract, designed first): part two: a saved frame transports missingService across a change in the requirement row (decisions row 117)
Requirement R9: Well-typed programs never go wrongabout:req:R9
This page explains requirement R9 in Effect4. It covers what the requirement asks for type safety and defect exclusion, why non-halting matters, and how the property is checked.
What the requirement asksabout:req:R9:what-it-asks
Requirement R9 formalizes type safety by proving that every typed program execution satisfies ExitOk and never halts (docs/core/system-map. §8, DB-16):
- Exit correctness:
ExitOk w ty ex := FitsExit w ty ex ∧ NoShapeDefect ty exholds at every typed exit position. - Shape defect exclusion:
NoShapeDefectexcludes reserved malformed code defects such asbadNameandnotImplemented(decisions row 107). - Non-halting: the small-step transition system never encounters a stuck configuration (
machineTyped_not_halted).
The property is scoped to M7Fragment: a lawful source, an empty row table, an admitted closed program, and an answer-free tape.
Why it mattersabout:req:R9:why-it-matters
Type systems aim to prove that well-typed programs cannot go wrong (Milner 1978).
In untyped JavaScript, unhandled shapes, missing services, and internal runtime bugs cause unexpected crashes.
Requirement R9 asks that a checked program end in a value or a typed cause, and never halt the machine.
How it is checkedabout:req:R9:how-it-is-checked
The requirement is checked by assembling the milestone proofs M5, M6, and M7:
- The route theorem
m7_of_ledgerstates that load typing (M5) and the preservation ofConfigTypedby each command (M6) imply milestone M7 (src/Effect4/Laws/Program/Typed/Assembly.).lean - The theorem
machineTyped_not_halted, in the same file, states that a typed machine is never halted. - Milestone results are stated by
m7_provedinsrc/Effect4/Laws/Program/Typed/Commands/Clauses/All..lean - Source program admission connecting checked programs to M7 is stated by
m7_admitted(src/Effect4/Laws/Program/Typed/AdmittedSource.).lean
The plan on this page gives each theorem's status and the goals it rests on.
The figure in words
- m7_admitted modulo → m7_proved
- m7_proved modulo → decision_preserves
- decision_preserves modulo → deliver_preserves, loop_preserves
- deliver_preserves modulo → countdown_parks_positional
- loop_preserves modulo → countdown_parks_positional
- countdown_parks_positional goal
The figure in words
- No concept open, 25 nodes, 5 open → Residual Program Typing, Store Typing, Subtyping Algebra, Reactive Scheduling, Initial Algebras & Folds, Scope Lifetime & Finalization, Exact Codecs
- Reactive Scheduling open, 2 nodes, 1 open
- Residual Program Typing proved, 18 nodes → Initial Algebras & Folds, Store Typing, Subtyping Algebra, No concept, Exact Codecs
- Store Typing proved, 12 nodes → Subtyping Algebra, No concept
- Subtyping Algebra proved, 44 nodes → No concept
- Initial Algebras & Folds proved, 4 nodes → No concept
- Scope Lifetime & Finalization proved, 4 nodes → Store Typing, Subtyping Algebra, Residual Program Typing, Initial Algebras & Folds, No concept
- Exact Codecs proved, 1 nodes
| Node | Status | Rests on | Nearest nodes |
|---|---|---|---|
m7_proved | modulo | countdown_parks_positional | decision_preserves, loadsTyped, m7_of_ledger |
m7_admitted | modulo | countdown_parks_positional | m7_proved, lawfulSig_of_admitted |
countdown_parks_positional | goal | countdown_parks_positional | — |
decision_preserves | modulo | countdown_parks_positional | fits_subN, satisfies_empty, order_refl, fits_mono, order_trans, mono, subN_trans, configTyped_frame, hom_eq_cata_ty, wake_preserves, close_typed, seq_typed, registrationDone_preserves, launch_preserves, subN_never, guardBind_typed, deliver_preserves, loop_preserves, driveState_lift |
loadsTyped | proved | — | denotesTyped, checkModule_eq_check, check_complete, checkModule_sound, satisfies_empty |
m7_of_ledger | proved | — | at_append, order_trans, order_refl |
lawfulSig_of_admitted | proved | — | admitSig_ok_iff |
fits_subN | proved | — | subN_trans, fits_normalize |
satisfies_empty | proved | — | — |
order_refl | proved | — | — |
fits_mono | proved | — | — |
order_trans | proved | — | — |
mono | proved | — | order_trans |
subN_trans | proved | — | — |
configTyped_frame | proved | — | satisfies_empty, fits_mono, order_trans, mono, order_refl, hom_eq_cata_ty |
hom_eq_cata_ty | proved | — | — |
wake_preserves | proved | — | order_refl, configTyped_frame, fits_mono, completionStrong_await, hom_eq_cata_ty |
close_typed | proved | — | — |
seq_typed | proved | — | subN_refl, fits_subN, guardBind_typed |
registrationDone_preserves | proved | — | order_refl, fits_mono, order_trans, mono, satisfies_empty, close_typed, fits_subN |
launch_preserves | proved | — | subN_refl, fits_subN, satisfies_empty, order_refl, fits_mono, order_trans, mono, satisfies_weaken |
subN_never | proved | — | — |
guardBind_typed | proved | — | — |
deliver_preserves | modulo | countdown_parks_positional | order_refl, satisfies_empty, fits_mono, order_trans, mono, satisfies_weaken, settle_callback, hom_eq_cata_ty, completionStrong_await, memoBuild_extension, deferredMake_extension, refMake_extension, subN_never, fits_subN, scopeParams_child, at_child, denotesTyped, listOf_upper, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, subN_refl, at_append, scopeParams_below, fiberTy_upper, matchB_sound, syncRow_typed, withParams_of_none, errOf_payload, isPayload_of_hasTy_record, foreignFinalizer_ambient, fits_scope_inv, seq_typed, closeSeqProtocol, configTyped_frame, close_typed, clause_scoped, clause_closeScope, scopeParams_ref, scopeParams_layer_below, satisfies_union, withParams_serviceTy, guardBind_typed, countdown_parks_positional |
loop_preserves | modulo | countdown_parks_positional | order_refl, satisfies_empty, fits_mono, order_trans, mono, satisfies_weaken, settle_callback, hom_eq_cata_ty, completionStrong_await, memoBuild_extension, deferredMake_extension, refMake_extension, subN_never, fits_subN, scopeParams_child, at_child, denotesTyped, listOf_upper, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, subN_refl, at_append, scopeParams_below, fiberTy_upper, matchB_sound, syncRow_typed, withParams_of_none, errOf_payload, isPayload_of_hasTy_record, foreignFinalizer_ambient, fits_scope_inv, seq_typed, closeSeqProtocol, configTyped_frame, close_typed, clause_scoped, clause_closeScope, scopeParams_ref, scopeParams_layer_below, satisfies_union, withParams_serviceTy, guardBind_typed, countdown_parks_positional |
driveState_lift | proved | — | — |
denotesTyped | proved | — | provideLayerArm, at_child, subN_refl, fits_subN, fits_normalize, fiberTy_upper, scopeParams_child, hom_eq_cata_ty, subN_trans, matchB_sound, syncRow_typed, withParams_of_none, listOf_upper, normalize_idem, lift_sound, causeInputError_upper, matchArgsB_sound, errOf_payload, isPayload_of_hasTy_record, satisfies_weaken, subN_never, fits_mono, order_trans, invoke_arm, optionTy_upper, withParams_serviceTy, scopeParams_below, exitOf_upper, fits_scope_inv, param_arm, call_arm |
checkModule_eq_check | proved | — | — |
check_complete | proved | — | — |
checkModule_sound | proved | — | check_sound |
at_append | proved | — | — |
admitSig_ok_iff | proved | — | — |
fits_normalize | proved | — | subN_trans, normalize_idem |
completionStrong_await | proved | — | subN_trans |
subN_refl | proved | — | — |
satisfies_weaken | proved | — | — |
settle_callback | proved | — | fits_subN, fits_mono, subN_never, subN_refl, order_refl, scopeParams_child, at_child, order_trans, fits_scope_inv, seq_typed, closeOrder_eq, mono, satisfies_empty, configTyped_frame, hom_eq_cata_ty |
memoBuild_extension | proved | — | — |
deferredMake_extension | proved | — | — |
refMake_extension | proved | — | — |
scopeParams_child | proved | — | — |
at_child | proved | — | at_append |
listOf_upper | proved | — | list_eliminator, normalize_idem, subN_trans, subN_refl, extendAll_upper |
normalize_idem | proved | — | — |
lift_sound | proved | — | lift_transfer |
causeInputError_upper | proved | — | cause_upper, cause_mono, normalize_idem, subN_trans, subN_refl, UnionRule., subN_causeOf_causeUpper, subN_exitOf_causeUpper, extendAll_eq_some_iff |
matchArgsB_sound | proved | — | — |
scopeParams_below | proved | — | — |
fiberTy_upper | proved | — | fiber_eliminator, normalize_idem, subN_trans, subN_refl, extendAll_upper |
matchB_sound | proved | — | lookup_solve_seed |
syncRow_typed | proved | — | fits_normalize, subN_trans, fits_subN, termMaps_of_typed, matchB_sound, hom_eq_cata_ty, errOf_payload, isPayload_of_hasTy_record, normalize_idem, subN_refl |
withParams_of_none | proved | — | — |
errOf_payload | proved | — | — |
isPayload_of_hasTy_record | proved | — | handles_of_payloadFieldTy |
foreignFinalizer_ambient | proved | — | subN_never, fits_subN, fits_mono, order_refl, scopeParams_child, at_child, order_trans |
fits_scope_inv | proved | — | — |
closeSeqProtocol | proved | — | order_trans, fits_mono |
clause_scoped | proved | — | fits_mono, order_trans, mono, order_refl, satisfies_empty, denotesTyped, configTyped_frame, hom_eq_cata_ty |
clause_closeScope | proved | — | fits_mono, order_trans, mono, subN_never, fits_subN, order_refl, scopeParams_child, at_child, fits_scope_inv, seq_typed, closeOrder_eq, satisfies_empty, configTyped_frame, hom_eq_cata_ty |
scopeParams_ref | proved | — | — |
scopeParams_layer_below | proved | — | — |
satisfies_union | proved | — | — |
withParams_serviceTy | proved | — | — |
provideLayerArm | proved | — | fits_subN, subN_refl, fits_normalize, fiberTy_upper, scopeParams_child, at_child, hom_eq_cata_ty, subN_trans, matchB_sound, syncRow_typed, withParams_of_none, listOf_upper, normalize_idem, lift_sound, causeInputError_upper, matchArgsB_sound, errOf_payload, isPayload_of_hasTy_record, satisfies_weaken, subN_never, fits_mono, order_trans, fits_scope_inv |
invoke_arm | proved | — | normalize_idem, fits_mono, fits_subN, order_trans, at_child, scopeParams_below, listOf_upper, fits_normalize, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty, scopeParams_body, withParams_defOf |
optionTy_upper | proved | — | option_eliminator, normalize_idem, subN_trans, subN_refl, Eliminator. |
exitOf_upper | proved | — | exit_eliminator, normalize_idem, subN_trans, subN_refl, extendAll_upper |
param_arm | proved | — | normalize_idem, fits_mono, fits_subN, order_trans, listOf_upper, fits_normalize, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty, scopeParams_decl, withParams_param |
call_arm | proved | — | fits_mono, fits_subN, normalize_idem, order_trans, listOf_upper, fits_normalize, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty, scopeParams_body, withParams_of_none |
check_sound | proved | — | — |
closeOrder_eq | proved | — | — |
list_eliminator | proved | — | subN_list_iff, normalize_idem, subN_trans, subN_refl |
extendAll_upper | proved | — | extendAll_adjoint |
lift_transfer | proved | — | joinAll_keeps, mapM_answer |
cause_upper | proved | — | subN_causeOf_causeUpper, subN_exitOf_causeUpper |
cause_mono | proved | — | subN_exitOf_iff, subN_causeOf_causeUpper, subN_trans, subN_causeOf_iff |
UnionRule. | proved | — | le_joinAll, subN_trans, mapM_answer |
subN_causeOf_causeUpper | proved | — | — |
subN_exitOf_causeUpper | proved | — | subN_trans, subN_refl, subN_exitOf_iff |
extendAll_eq_some_iff | proved | — | — |
fiber_eliminator | proved | — | subN_fiberOf_iff, normalize_idem, subN_trans, subN_refl |
lookup_solve_seed | proved | — | — |
termMaps_of_typed | proved | — | listOf_upper, fits_subN, fits_normalize, normalize_idem, lift_sound, subN_trans, causeInputError_upper, matchArgsB_sound, hom_eq_cata_ty, fits_mono |
handles_of_payloadFieldTy | proved | — | — |
scopeParams_body | proved | — | — |
withParams_defOf | proved | — | — |
option_eliminator | proved | — | subN_option_iff, normalize_idem, subN_trans, subN_refl |
Eliminator. | proved | — | subN_refl, UnionRule. |
exit_eliminator | proved | — | subN_exitOf_iff, normalize_idem, subN_trans, subN_refl |
scopeParams_decl | proved | — | — |
withParams_param | proved | — | — |
subN_list_iff | proved | — | — |
extendAll_adjoint | proved | — | adjoint, extendAll_eq_some_iff |
joinAll_keeps | proved | — | foldl_keeps |
mapM_answer | proved | — | mapM_cons_eq_some |
subN_exitOf_iff | proved | — | — |
subN_causeOf_iff | proved | — | — |
le_joinAll | proved | — | joinAll_keeps |
subN_fiberOf_iff | proved | — | — |
subN_option_iff | proved | — | — |
adjoint | proved | — | Eliminator., subN_trans, mapM_total, Eliminator. |
foldl_keeps | proved | — | — |
mapM_cons_eq_some | proved | — | — |
Eliminator. | proved | — | UnionRule. |
mapM_total | proved | — | mapM_cons_eq_some |
UnionRule. | proved | — | subN_trans, mapM_source, joinAll_le |
mapM_source | proved | — | mapM_cons_eq_some |
joinAll_le | proved | — | joinAll_all |
joinAll_all | proved | — | foldl_all |
foldl_all | proved | — | — |