The KeY Project | Hacker News Reader

The KeY Project

key-project.org

50 pointsTomte10 comments

Looks interesting, surprised to see it runs on Eclipse. I had to try Eclipse again for Garmin after years of not using it. Man Eclipse is buggier and less useful than I remembered it being. I love IntelliJ and can't replace it, my only exception would be Neovim (which I'm still waiting on JetBrains to allow embedding) or VS Code.

Anybody used it? I attended the lecture "introduction to formal methods" by one of the profs behing the project at KIT. It was a fantastic lecture and the prof was very good, but the scriptum was 600 pages long just for a few ECTS. I always wondered whether this project has industrial use somewhere or not.

The timsort bug:

http://www.envisage-project.eu/proving-android-java-and-pyth...

Most software that's correctness critical is not written in Java.

But I could see KeY-verified voting machines as at least better than the status quo (as long as you take it as an assumption that for whatever reason we absolutely need voting machines).

But alas:

> The reaction of the Java developer community to our report is somewhat disappointing: instead of using our fixed (and verified!) version of mergeCollapse(), they opted to increase the allocated runLen “sufficiently”. As we showed, this is not necessary. In consequence, whoever uses java.utils.Collection.sort() is forced to over allocate space.

One I found on the website:

https://www.key-project.org/2018/02/13/keys-sed-successfully...

In an interesting coincidence, Hillel Wayne just did a write-up on applying Alloy to a similar scenario:

https://www.hillelwayne.com/post/formally-modeling-migration...

So is it only usable for testing/verifying Java code?

Yes, this is only for Java.

Post could profit from a rename since it's about the KeY project and the current title is only a tagline that's not expanded on further.

The tagline tells you what it's about. The project name doesn't tell you anything at all.

The real key to software correctness is to use homotopy type theory, not java.

Reply on news.ycombinator.com