PSBP library and documentation

Stream: computer science

[Luc Duponcheel]

Hello, folks, I already posted about PSBP in the general topic.
A member of the Lean community suggested me to also post in this computer sciencetopic.

see
https://github.com/LucDuponcheelAtGitHub/PSBP
for code
see
https://github.com/LucDuponcheelAtGitHub/psbpDocumentation
for documentation

You'll have to build the documentation locally yourself as
explained in the README.md.

I am working on a "github.io" site.

The content is now

1. About
2. Naming conventions
3. Programs versus Computations
4. The PSBP library type classes
5. fibonacci and factorial
6. Laws
7. Computation Valued Functions
8. Theorems
9. ActiveProgram
10. ReactiveProgram
11. Positional Programming
12. Programming With State
13. Programming With Failure

Hopefully the set of interested computer scientists is not empty.
All comments are welcome.

[Luc Duponcheel]

You may wonder why I do this PSBP (Program Description Based Programming) project. Just like computations (monads) are effectful expression specifications, (what I call) programs are effectful function specifications. 32 years ago I worked on the fundaments of computations and computation transformers at the University of Utrecht. Computations (monads) are mainstream now in many programming language libraries. Now that I am retired, I think that programs are the way to go. Why? Well because computations (and expression) are operational artifacts, while programs (and functions) are denotational artifacts (they have a meaning and can be given a meaningful name). For example, the associativity law of computations is an operational law (and difficult to remember). The associativity law of programs is a denotational law (and easy to remember).

[Luc Duponcheel]

Hello folks, I decided to document the PSBP library in the README.md file of the PSBP repository itself. Agreed, a bit more "low profile" than other Lean documentation. The documentation is also a kind of course with exercises and solutions.

Once again, sorry for all my posts, hopefully the set of interested people is not empty. And, once again, all comments are welcome.