remember, boys n girls, there's no lang that has rigorous math-like doc or spec. None. xahlee.info/comp/blog.html

@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
No Agenda Social

Home to Producers and Fans of the
No Agenda Show Podcast If you have an issue please DM @[email protected]