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

in programing, if you spend 1 min with with good doc, you spend 1 hour without, or even 10. When there's no doc, 10 days.

@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