Alloy is a language for describing structures and a tool for exploring them
11–20 of 23 posts
Re: Alloy is a language for describing structures and a tool for exploring them
#12There was a fantastic talk at strangeloop this year on Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ . The speaker used it to find a serious security bug in their live code and a feature interaction bug in their UI that had meant they had been writing broken code for the past _year_. (full disclosure I'm referenced towards the end)
I watched that earlier this week, and have been making my way through the Software Abstractions book by Jackson. Alloy's still in the "this thing makes me feel stupid" territory, but it does feel learn-able to me. I really like the emphasis on iterative development.
I found Jackson’s book excellent, one of the most readable books with the depth the book had.
Re: Alloy is a language for describing structures and a tool for exploring them
#13Last week Microsoft Research posted an interesting talk by Kevin Buzzard [1] from Imperial College London about how he wants to formalize all mathematics with theorem provers. He's currently using LEAN [2]. Half of the talk is a discussion of the challenges he's faced convincing other mathematicians that this is valuable, and the other half is about his success using LEAN as a tool to teach undergraduates about forma…
Convincing mathematicians about it is a really old problem. Here's the first paper I saw really describing how mathematics has been done as a social process focused on people's understanding:
https://www.cs.cmu.edu/~pattis/misc/socialproofs.pdf
A 2009 rebuttal to be fair to my side of the debate:
https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=40...
Here's a recent article about the situation from yet another segment of people trying to bring in automation:
https://www.quantamagazine.org/in-computers-we-trust-2013022...
Unlike article's impression, a lot of how to build trustworthy provers has already been solved. The state-of-the-art is probably Milawa: a prover for ACL2-like logic running on a Lisp verified down to the machine code. It has summaries of various approaches of making computational math/logic trustworthy:
https://www.kookamara.com/jared/2015-jar-milawa.pdf
Note: Like in Common Criteria EAL7 or DO-178C, I'd use a mix of techniques for verification instead of blindly trusting the math. Lots of human review, static analysis, testing, etc.
Far as projects implementing math's foundations, you should especially check out Mizar (most complete) and Metamath (open source):
https://en.wikipedia.org/wiki/Mizar_system
https://en.wikipedia.org/wiki/Metamath
If authors give permission, it might be worthwhile to attempt to create re-writing tools that convert those tools languages into platforms in use by programmers. That's mainly Coq, the HOL's, Why3, and (hardware) ACL2. I don't know how feasible that is. I just think it could be valuable.
Re: Alloy is a language for describing structures and a tool for exploring them
#14Forgive my ignorance, but after looking at the Github readme I'm not really understanding what this does. What kinds of things would Alloy be used for?
Re: Alloy is a language for describing structures and a tool for exploring them
#15In what way is this alloy different than the official/original alloy? This the official alloy now?
There is literally no mention or prior credit on your site to the original? A lot of unanswered things here.
Re: Alloy is a language for describing structures and a tool for exploring them
#16Forgive my ignorance, but after looking at the Github readme I'm not really understanding what this does . What kinds of things would Alloy be used for?
Here’s a good intro from strangeloop: https://www.youtube.com/watch?v=FvNRlE4E9QQ
Re: Alloy is a language for describing structures and a tool for exploring them
#17In what way is this alloy different than the official/original alloy? This the official alloy now? There is literally no mention or prior credit on your site to the original? A lot of unanswered things here. http://alloy.lcs.mit.edu/
I've been wondering about this for a while. This one shows up ranked fairly highly on Google searches for alloy. I was very confused but I suspect it's an identically or confusingly named fork. But when I first discovered it, I spent a while assuming that development had just migrated to GitHub.
Has the original alloy gone unmaintained?
Re: Alloy is a language for describing structures and a tool for exploring them
#18In what way is this alloy different than the official/original alloy? This the official alloy now? There is literally no mention or prior credit on your site to the original? A lot of unanswered things here. http://alloy.lcs.mit.edu/
I've been wondering about this for a while. This one shows up ranked fairly highly on Google searches for alloy. I was very confused but I suspect it's an identically or confusingly named fork. But when I first discovered it, I spent a while assuming that development had just migrated to GitHub. Has the original alloy gone unmaintained?
In any case if it has, in my personal opinion it's quite shady to fork a project and remove all reference to the pre-fork, except the cover of the book, which is just a picture and not even a link to the original MIT site.
Re: Alloy is a language for describing structures and a tool for exploring them
#19In what way is this alloy different than the official/original alloy? This the official alloy now? There is literally no mention or prior credit on your site to the original? A lot of unanswered things here. http://alloy.lcs.mit.edu/
Check the "Downloads" page at the MIT site. The "Experimental versions -- latest build" link points back to the Github site in question. (I agree that the Github site should explain the relationship.)
Re: Alloy is a language for describing structures and a tool for exploring them
#20In what way is this alloy different than the official/original alloy? This the official alloy now? There is literally no mention or prior credit on your site to the original? A lot of unanswered things here. http://alloy.lcs.mit.edu/
It's the exact same people, and alloytools.org is now the official site. I agree that it's confusing and let people know that we need a redirect or notice on the old site.