- Author
- Not stated
- Published
- Undated
- Kind
- Documentation chapter introduction from an online tutorial book
- Original
- fstar-lang.org/tutorial/book/part4/part4.html
- Subject
- Checkable specs for coding agents
- Themes
- Checking the work
What it is
The page opens the effects part of a Sphinx-built tutorial book on F*. The footer credits Microsoft Research. It introduces F*'s effect system for programs that do more than return a value.
What it says
- The page says pure programs act like math functions. Only the returned value is observable.
- The page says real programs mutate state, touch files or use the network. These behaviors are called effects.
- The page says F*'s effect system lets users model effects and prove things about them.
- The page lists three primitive effects: Ghost, Divergence and Partiality.
- The page says the Ghost effect marks parts of a program that can be erased.
What evidence it gives
The page offers definitions only. It has no code, proofs or examples. A footnote notes that pure programs still use time, power and memory.
Interests and limits
The page is a short section introduction, so most detail sits in its subpages. Those subpages were not read. The sidebar chapter on agentic proof-oriented programming was also not opened. The page is an official project doc, so it describes F* favorably by design.