20. Open questions
Each question has the options, the default that the build uses until a decision, and the measurement or event that decides it. A decision is a pull request on this document and on the documents that it changes.
| # | Question | Options | Default | Decided by |
|---|---|---|---|---|
| Q-01 | The licence of implementations, tests and scenes | MIT; MIT-0 or 0BSD (no attribution); Apache-2.0 (as the toolchain) | MIT (17.1): the licence that most developers know, and the one of TheAlgorithms | feedback from the first 100 issues; if many readers ask to copy with no notice, MIT-0 |
| Q-02 | Do algorithm and math2 share one tag register? | one register for both; two registers with the same alphabet and different URI schemes | two registers, al:// and m2://; a link names its scheme |
if a third project needs shared tags, a shared register service |
| Q-03 | Kotlin or Swift in tier 1 | Kotlin; Swift; both (11 languages) | Kotlin (08.2): it is used on Android, on the server and in competitive programming; Swift is tier 2 | the share of language tab clicks in M2–M3; a tier 2 language with more clicks than a tier 1 language for two months moves up |
| Q-04 | Where the formal work lives | our package Algo that depends on CSLib; contribute everything to CSLib |
Algo on top of CSLib, with general lemmas and algorithms upstreamed (07) |
the CSLib maintainers' wishes on breadth and naming; reviewed at each release |
| Q-05 | Aeneas and the Lean pin | the same pin for everything; a separate workspace for L4 with the Lean version of Aeneas | a separate workspace lean-aeneas/ when the versions differ; its theorems restate the model's statement by its hash |
the first Aeneas release that supports the pinned Lean version |
| Q-06 | The rendering of scenes | SVG; Canvas; WebGL | SVG up to about 2,000 elements, Canvas above (10) | frame rate measured on a low-end phone in M2 |
| Q-07 | Search | static index only; a Worker with D1 FTS5; a Worker with vector search for "I need to…" | static only (15) | the evaluation set of 15: if the static index misses the target in the top 5 for more than 10% of the natural-language queries, add the Worker |
| Q-08 | Language pages | a URL for each language of each algorithm; tabs only | a URL for tier 1 and tier 2, tabs on the main page (14.2) | the file budget (14.9) and search traffic to language pages after M2 |
| Q-09 | Auto-merge of agent code | never; after all gates and a jury pass; after all gates only | after all gates and a jury pass, for implementations of nodes whose contract a person reviewed (12) | the defect rate found by human sampling (13.4): above 1% of auto-merged files, stop auto-merge |
| Q-10 | The oracle when a problem has no Lean model yet | a Python reference reviewed by a person; the agreement of 3 implementations | a reviewed Python reference (09.5) | when the Lean model lands, the oracle switches, and any difference is a finding |
| Q-11 | Languages of the text | English only; English and Vietnamese; English and Chinese and Vietnamese | English only until M4; aliases in all languages from M1 | the reader statistics by country after M3 |
| Q-12 | The style of pseudocode | CLRS style; Python-like; our own small language | our own small language with stable line ids (06) | a review by 3 teachers of the gold set in M0 |
| Q-13 | Complexity checks as a gate | gate; report only; gate on gross mismatches only | gate on gross mismatches only (09.7) | the false positive rate on the gold set and the core in M2 |
| Q-14 | One content repository or several | one; one per area; one for code and one for text | one, re-checked at 2 GB or when a clone takes more than 2 minutes | the size report in each release |
| Q-15 | Exercises from LeetCode | links with metadata; links only; none | links with title and difficulty only (11.4) | the terms of the site at each harvest |
| Q-16 | Cryptographic implementations | all, as for other areas; tier 1 only; none | tier 1 only, marked "for learning, not for production", with no constant-time claim (17) | an issue from a security reviewer |
| Q-17 | The name on the site | "Algorithm"; "Algorithms"; "Algorithm 2.0" | "Algorithm", after the domain | the maintainer |
| Q-18 | Human review capacity | the maintainer only; invited reviewers; open review with a register of reviewers as in math2 | a register of reviewers (registers/reviewers.reg) from M2, with the maintainer as the first |
the review backlog: if more than 500 items wait, invite reviewers by area |
| Q-19 | Proof of average-case and expected bounds in Lean | prove them in a probability monad on top of TimeM; prove worst case only |
worst case and amortized only until CSLib has randomized algorithms (planned for 2027) | the CSLib release with a probabilistic cost model |
| Q-20 | Parallel and distributed cost claims | prove work and span in Lean; state them with a human proof only | human proof only for work, span, rounds and messages until a model exists in CSLib | as Q-19 |
| Q-21 | Space bounds in Lean | wait for a space monad in CSLib; our own Algo.Cost.SpaceM; no space claims in Lean |
Algo.Cost.SpaceM, a high-water mark of allocated cells, used only when a node sets lean.space: true (07.4) |
a CSLib release with a space model; then SpaceM proofs are ported and the type is retired |
| Q-22 | Refinement for languages other than Rust | Verus (Rust), Dafny, Why3; none | none in this version: L4 is Rust through Aeneas only, and the other languages are tied to the model by the differential tests (07.6, 09.5) | the share of L4 work done on Rust at M4; if a second language is asked for, Verus first, because it shares the Rust sources |
| Q-23 | The renderer of Lean modules | Verso with SubVerso; SubVerso exports with our own templates; plain highlighted source | SubVerso exports with our own templates (07.16, 14.7.7), with Verso as the model for the look | if SubVerso does not support the pinned Lean version at a bump, the fallback is plain highlighting with hovers from AlgoExtract, so a bump never waits on the renderer |
| Q-24 | The languages of aliases | the 12 languages of 15.6; every language that Wikidata has; English only | the 12 languages of 15.6 (English, Chinese, Spanish, Russian, Japanese, Portuguese, German, French, Korean, Vietnamese, Hindi, Turkish) | search logs of queries with no result after M2; a language with more than 1% of such queries joins |
| Q-25 | The search engine in the browser | our own matcher (15.5); MiniSearch; Lunr; Pagefind for everything | our own matcher for the palette, about 6 KB gzip, with Pagefind for full text from M3 (15.9) | the evaluation of 15.8: if a library gives the same success at 5 with a smaller or equal download, it replaces ours |
| Q-26 | Patents | a register of patents that may still be in force, with a note on the page; no notes; no pages for such algorithms | a register registers/patents.yaml and a neutral note on the page, with no legal advice (17.5) |
a request from a rights holder or a contributor's lawyer |
| Q-27 | The export notice for cryptography | a notice to the US authorities once for the repository, as the EAR allow for public source code; no notice | a notice once, as of 17.5, before the first cryptography implementation lands | advice from counsel at M2, before the cryptography area is written at scale |
| Q-28 | The licence of machine-made parts | the licence of the zone, as for human work; CC0 for parts that no person changed | the licence of the zone (17.4), with "The algorithm contributors" as holder | a change in the law or in the US Copyright Office's guidance on machine-made material |
| Q-29 | Contributor agreement | DCO sign-off only; a CLA | DCO only, no CLA (17.1), as in math2 | a need to relicense a zone; a CLA would be needed only then, and Q-01 would come first |