The Laestrygonian harbor from the epic Odyssey is a narrow-basin trap with a single restricted entrance. We are interested to find out what rule or policy keeps a fleet from entering a place where escape is an impossibility later on.
The harbour has a small entrance, steep sides, and a closed basin. Once a ship moves inside and takes a moored position, the space to turn or leave becomes very small and there isn’t enough room to react. Here is where Lean helps to make a decision by turning the story into precise rules.
Harbor state can be written as ‘safe’ or ‘unsafe’. A ship’s action can be written as enter, moor or escape. Lean checks a rule in this manner,
“if enter basin and moor then escape may fail“,
asking what conditions make the failure unavoidable.
By exposing the trap conditions and by evalutating a combination of narrow openings, a bounded basin, and mooring inside can produce a state where escape is not feasible. If the policy allows those steps, the policy is incomplete.
A safer set of rules should at least account for -
1) Not to moor inside a closed basin
2) Don’t enter moor unless an exit path remains open
3) Avoid scenarios where all ships might end up boxed in
Using lean we get a peak into intricacies of dependent types in functional languages through a scenario of an epic like Odyssey that has enriched humanity since before common era, turning an unclear safety idea into a clear picture, especially relevant in uncertain current times where passing through a strait has its share of catastrophic dangers.
Verification is needed because a policy can sound reasonable while still allowing for a bad outcome to occur. We circumvent that with Lean which pre-empts the unfavourable outcome.
