dafny icon indicating copy to clipboard operation
dafny copied to clipboard

New Logo for Dafny

Open booniepepper opened this issue 2 years ago • 17 comments

What change in documentation do you suggest?

I love Dafny as what I feel is the most working-programmer-friendly proof language, a fun joint-venture between academia and industry.

The current logo is interesting and thought-provoking; even bold! ...but I can't exactly place what it's supposed to signify. Hairy beach-side mountains? A person in the water?

I'd like to be able to propose a new logo for Dafny, and release them in SVG format to the Dafny project under its license, or a license of the project owner's choosing.

Before I (or anyone else) actually proposes any images, I have at least two questions:

  1. What's the inspiration for the name "Dafny"? I couldn't find this in the website, manual or blog. Is it a reference to Daphne?

  2. What's the current logo actually intending to convey?

booniepepper avatar Jul 23 '23 05:07 booniepepper

P.S. "Not interested right now" is totally valid too, and I wouldn't be offended.

booniepepper avatar Jul 23 '23 05:07 booniepepper

Totally interested! Let me ask around what Dafny stands for again. I believe it's partly an acronym

keyboardDrummer avatar Jul 24 '23 14:07 keyboardDrummer

There is already another logo for Dafny made by a designer that we use for the documentation: https://dafny.org/images/dafny-favicon.svg

MikaelMayer avatar Jul 24 '23 15:07 MikaelMayer

The name Dafny comes from scrambling the first letters of "DYNamic FrAmes". Dafny was initially created to experiment with the "dynamic frames" style of specifying programs that work with the heap. Dynamic frames are still part of Dafny, but with all of the uses and capabilities of Dafny today, dynamic frames have not been the central part of Dafny for a long time. Since Dafny is a Greek-sounding name, it was also especially appropriate, because the person who invited dynamic frames, Yannis Kassios, is Greek. The current logo shows a person by the (possibly Greek) sea.

RustanLeino avatar Jul 24 '23 15:07 RustanLeino

Thanks all! I'm letting this stew in my brain for a little while

booniepepper avatar Jul 26 '23 17:07 booniepepper

Here are some early ideas based on "a tree by the sea" taking some inspiration from the current logo and also the legend of Daphne (a nymph: so water) who was turned into a laurel tree on her own request (which is... kinda like verification causing the resulting software more durable?)

Not sure about the color scheme. It's roughly brown = tree trunk, blue = sea, green = sky or laurel leaves

BTW I made a repository to hold ideas while I'm thinking this over https://github.com/booniepepper/dafny-logo-ideas/tree/core

Next time inspiration strikes, I might try to incorporate the whole word "Dafny" instead of just the leading D

booniepepper avatar Jul 28 '23 06:07 booniepepper

I love the idea of creating a new logo, and your logo and suggestions are very interesting. The logo is a bit tern (to me), could you increase saturation a bit and perhaps make it lighter? Can't wait to see other suggestions.

MikaelMayer avatar Jul 28 '23 20:07 MikaelMayer

Brighter variations! Brown is weird especially wrt saturation but let's go anyway

Also snuck in one more complex idea along the same kind of "letter D and water/tree" theme, but with the water more actively turning into a tree.

booniepepper avatar Aug 01 '23 06:08 booniepepper

Nice attempts! I'd definitely lean towards the one on the left, but I like your second as well.

MikaelMayer avatar Aug 01 '23 14:08 MikaelMayer

Still thinking about this. Have been out of country for a while visiting family. Might have some more sketches to flesh out in Sept/Oct

booniepepper avatar Aug 24 '23 14:08 booniepepper

Personally I like the old and admittedly weird logo. I personally dislike that all languages and technologies needs to be branded in the same sense as commodities have to be. One of the things that gets me excited about formal verification is that it yet appears to exist outside of the absolute nightmare that is the commodification of everything related to computer science.

TheGrandmother avatar Sep 06 '23 11:09 TheGrandmother

Thanks for chiming in! I do like the punk/diy vibe that the previous logo has going for it. I also agree that a logo doesn't have to be slick or modern or beautiful or minimalist or anything like that really. Graphic design and illustration are just a hobby of mine, I'm a software engineer by trade. That said, the key points for me are that a logo should be both memorable and recognizable, and I believe that's useful. I think this is where the current logo is falling for me. It should not be forgettable or hard to recognize. A lot of this is subjective but for me this is where the current logo is lacking

As a side note, I think this kind of punk/diy feeling can be done really well, for example OpenBSD has a recognizable mascot that's intentionally not beautiful or polished. The art for each release is always a different style, and so many of them are memorable. https://www.openbsd.org/artwork.html

(Lots of opinion here) I think Dafny is only a bit rebellious: it takes formal verification and dares to make it look and feel like a working man's language instead of something more academic. That's pretty bold in my book, but it's also polished and ergonomic. It's more about being pragmatic than it is about being counter culture

(Side note: I'm still sort of just thinking this over. Currently traveling abroad and visiting family)

booniepepper avatar Sep 06 '23 13:09 booniepepper

Daymn, those old BSD artworks are amazing! Thanks for sharing!!! :)

And the logos you made are really cool! especially the tree one!

My objection to the dependance on a logo is not hat of being corporate or punk but rather the perceived need for branding. And the novelty value of having an odd logo outweighs any benefit that a good logo would have.

(100% subjective and unfounded opinions incoming) In my opinion formal verification is one of the most subversive things that one can do within the field of computer science. This is simply by virtue of standing in opposition (in my oppinion) to the overly optimistic and short term focused paradigms that exists within todays tech industry.

TheGrandmother avatar Sep 06 '23 14:09 TheGrandmother

Brighter variations! Brown is weird especially wrt saturation but let's go anyway

Also snuck in one more complex idea along the same kind of "letter D and water/tree" theme, but with the water more actively turning into a tree.

@booniepepper I love these! Personally, I'm leaning towards the one with the tree, it's so unique! If anything, I'd make the leaves a bit smaller and the trunks more clearly in the shape of a "D", but that's completely subjective. Great work!

ocramz avatar Mar 12 '24 16:03 ocramz

Ooooh... A few of us put our brains together, and I think we see the scene in the original logo now.

It's a sea contemplated by a person facing away from us, with only their shoulder line and long, wavy hair visible to us.

I would be curious to see the same idea realized in a more serious way. It looks like an MS Paint doodle. I assume this was the intended aesthetic, so I hope no offense is taken, but it sure is... humorous :)

2BitSalute avatar Jun 24 '24 03:06 2BitSalute

Sorry, I couldn't help it, but I went and tried generating one (more like 50, because I had to finesse the prompt to keep it from generating complicated designs) with Bing Image Creator, and a few I thought were pretty decent (to my taste). There's actually one that I'm not sharing that I'm going to use on one of my YouTube accounts :D

I'm impressed it managed to spell out "Dafny" correctly in some of the images. It didn't always succeed.

image

image

2BitSalute avatar Jun 24 '24 21:06 2BitSalute

Love these! I would vote for a simpler version of 4 or (8 without the light blue).

ocramz avatar Jun 25 '24 06:06 ocramz