remember, boys n girls, there's no lang that has rigorous math-like doc or spec. None.
#haskell #ocaml

@xahlee Dependent Typing with proposition-as-types and proofs-as-programs allows you to add formal specification and formal verification to code; Eg Idris, Coq, Agda.

@fabianhjr yes those are good.
but do they have documentation written as math text is written?


@xahlee depends if you are into Homotopy TT/Per Martin-Löf TT/Category Theory as foundations of mathematics.

Sign in to participate in the conversation is a cooperatively-run corner of the Fediverse. The instance is democratically governed by its members, who generally share an interest in the co-op model, but topics of discussion range widely.

If you are interested in joining our community, please review our Bylaws and Code of Conduct. If you agree with them, you may apply for membership on our instance via this link

Our instance is supported by sliding scale contributions of $1-10/mo made via Open Collective. You must have an active Open Collective account to apply for membership; you may set one up here