search

leanprover / leanprover.github.io

www
https://lean-lang.org/
15 stars 24 forks source link

[RFC] Begin restructuring the website #67

Closed jroesch closed 6 years ago

jroesch commented 7 years ago

This is a first draft at getting new content put on the website.

I prototyped a new home page, and setup the blogging infrastructure. I used the code that appeared to be there from Skinny Bones and added an author profile for myself.

The main todo is the Roadmap and communication guidelines.

I would love feedback on content & design, for example the stuff on the homepage is just quickly filled in, would be good to achieve some consensus about what we want there.

My hope is to do an initial restructuring of the website, then in the near future do a polish pass on the whole site. I think it may be time to update the CSS and redesign a little bit.

gebner commented 7 years ago

The homepage looks awesome!

jroesch commented 7 years ago

@gebner yeah the blog still needs to be fully written just had pasted some content in place, and we need to give some behavior to more examples. I just wanted to get some feedback on the high level design, and prose before investing more energy. I would also love to ship both a prototype reference and roadmap with the website update.

avigad commented 7 years ago

I have a number of concerns about the proposed changes. I think it is really important to get the web page right. For most people, it will provide their first impression of Lean, and first impressions stick around for a long time. It should be elegant and impressive.

There is a lot of information that will be helpful to users, and it is spread out over a lot of places (documentation, talks, forums and chat groups, the change log, etc., etc.). I think the main page should make it possible for users to find the information easily, but otherwise should be as simple as possible. Too much information that is not well maintained will make the project look like a mess. It is a mistake to try to add too much content, especially content that will quickly become outdated and stale.

For example, I think it is a bad idea to include developer bios. Lots of people have contributed to Lean, are contributing, and will contribute. Trying to maintain everyone's bio as their careers and interests change will be a nightmare, and then there are the concerns about how to uniformize the descriptions and what to do when people leave the project or become less active. There are a lot of associated headaches, and there is no pressing need. It is much easier to maintain a simple list of people involved, and anyone can use Google to find their web pages and learn about what they are doing.

I am not crazy about the characterization of Lean as a programming language designed for the development of safety critical software. That is a primary and important use, but it seems to sell the system short; Lean is much more general than that. I would characterize it as a logical foundation that can be used simultaneously as a specification language, programming language, proof language, metaprogramming language, and interactive platform for the use of flexible, verified automation.

We can tinker with the wording, but first let's try to settle on the overall design. Many of us will be in Cambridge next week. Perhaps we can have a discussion there? (@jroesch, we can include you remotely.)