Damn, this is the first time I've heard about Alloy, and I'm already really interested in it! Outside of applied computer science, technology like this could actually be really useful for lawyers, to get the facts straight of a court case, without overloading their brains, and letting the computer basically brute force tedious fact checks and possible scenarios. (Something like this might already exist, since the chance is fairly slim that I just came up with that idea, haha!)
Looks like youre talking about validation of specifications which should (normally) come BEFORE any line of code is produced. But what is true is your first statement : speaking/explaining to somebody else will bring you 99% of the time to your "Ah ah" moment ! I often explain to a imaginary guy and decide that its knowledge would be the same as me except he would not know anything about the project... and it helps a lot (I would say almost always).
This is useful if you have a massive system and/or you want to visualize the system in a glance reminds me of unit testing but without the visual diagrams and permutations and its scope is not just codes
The spec languages ideally should be mastered by managers or writing requirements :) . Or at least devs should be validating the informal spec as a first step after reading it.
This is a modeling tool, where you can find bugs on logical level. The code implementing the model might have issues, but you are able to catch logical problems way before it gets into the code, write test, deploy, QA, go to live, realize if the user presses the buttons in a particular order crashed everything.
@@rallokkcaz hello, I played a little bit with Alloy, but we need to handle time. I watched the other video and based on that Alloy way of handling of time is not very comfortable. What are your experiences? Thanks!
@@kardeskalap2165 I'm not knowledgeable in formal methods, but shouldn't A before B, B before A and order doesn't matter be enough to model most systems? I don't know if this can be expressed well in Alloy though. For example A before B, could mean, operation finishes before state B occurs, and B = "n seconds after A". And there would be some fact attaching time spans of each sub operation of A. I realize this sound a bit handwavy. I know there was at least one example of encoding computational complexity of a function using dependent types in Idris: th-cam.com/video/4i7KrG1Afbk/w-d-xo.html
I'd probably just BDD this or do some other kind of automated testing. The tool is neat and the counterexample use case is interesting but if it's not wired to the impl (or alive in a sense) then it's going to bit-rot like docs. The best thing about tests is that they (hopefully) go into CI and they live. I guess for experimentation this is a nice alternative but I don't like enterprise software that is so big that it can't be changed easily. What is a portal anyway? It's a website. Enterprise software is like this overly complex ceremony (not in all cases). I understand that it's easier said than done but ... man, software doesn't like scale/complexity.
I believe the closes analogy is that Alloy is a high-level "prototype". Not in the sense that it does what real prototype will, but it models the behaviour of your prototype. It's like a proof of concept that certain thing is possible. Very new lands to me, I wonder if it's possible to apply in my web development field(or stuff like Android/iOS programming). Stuff like modeling distributed consensus is great, but that's outside of the scope for me. That example with Users, Accounts, and Resources is closer to my every day worries.
Can Alloy be implemented as a virtual machine for use on top of popular software platforms for direct translation into javascript python C++ and java templates? Such tight integration would make rapid program trace and prototyping much more feasible
Alloy is just a checker, you could easily do annotations or something in most popular languages, write a tool that would build alloy models out of that and checked them. Or you could write a tool that would generate tests from alloy models. There is a ton of possibilities to make prototyping and programming better, but seems most people aren't interested to put time into that.
I think the solution that he doesn't give in minute 22:20 of the final example is pred can_access(u : User , r : Resource) { r in u.resources or some r" : Resource | r" in r.^parent and r" in u.resources } instead of pred can_access(u: User, r: Resource) { r in u.resources or (some r.parent and r.parent in u.resources) }
Note: this video inadvertently contains the house music track on the audio for the first minute or so. Apologies on that...
Awesome track, no apologies needed!
Damn, this is the first time I've heard about Alloy, and I'm already really interested in it!
Outside of applied computer science, technology like this could actually be really useful for lawyers, to get the facts straight of a court case, without overloading their brains, and letting the computer basically brute force tedious fact checks and possible scenarios.
(Something like this might already exist, since the chance is fairly slim that I just came up with that idea, haha!)
I feel like I stumbled upon motherlode of modern programming knowledge... Fantastic channel!
We are using a lot of static code analysis tools in our company. Intriguing to see that there are tools for verifying models hence designs, too.
Looks like youre talking about validation of specifications which should (normally) come BEFORE any line of code is produced.
But what is true is your first statement : speaking/explaining to somebody else will bring you 99% of the time to your "Ah ah" moment !
I often explain to a imaginary guy and decide that its knowledge would be the same as me except he would not know anything about the project... and it helps a lot (I would say almost always).
... his knowledge...
This is useful if you have a massive system and/or you want to visualize the system in a glance
reminds me of unit testing but without the visual diagrams and permutations and its scope is not just codes
The spec languages ideally should be mastered by managers or writing requirements :) . Or at least devs should be validating the informal spec as a first step after reading it.
So the alloy is a verification tool for the spec, which is agnostic to its implementation?
This is a modeling tool, where you can find bugs on logical level. The code implementing the model might have issues, but you are able to catch logical problems way before it gets into the code, write test, deploy, QA, go to live, realize if the user presses the buttons in a particular order crashed everything.
Very cool, would like to see how Alloy compares with TLA+ . I've tried TLA+ before, will be trying Alloy in the future!
Was gonna comment the same.
@@rallokkcaz hello, I played a little bit with Alloy, but we need to handle time. I watched the other video and based on that Alloy way of handling of time is not very comfortable. What are your experiences? Thanks!
@@kardeskalap2165 I'm not knowledgeable in formal methods, but shouldn't A before B, B before A and order doesn't matter be enough to model most systems? I don't know if this can be expressed well in Alloy though.
For example A before B, could mean, operation finishes before state B occurs, and B = "n seconds after A". And there would be some fact attaching time spans of each sub operation of A. I realize this sound a bit handwavy.
I know there was at least one example of encoding computational complexity of a function using dependent types in Idris: th-cam.com/video/4i7KrG1Afbk/w-d-xo.html
Super interesting! I'm definitely gonna have to experiment with this.
I'd probably just BDD this or do some other kind of automated testing. The tool is neat and the counterexample use case is interesting but if it's not wired to the impl (or alive in a sense) then it's going to bit-rot like docs. The best thing about tests is that they (hopefully) go into CI and they live. I guess for experimentation this is a nice alternative but I don't like enterprise software that is so big that it can't be changed easily. What is a portal anyway? It's a website. Enterprise software is like this overly complex ceremony (not in all cases). I understand that it's easier said than done but ... man, software doesn't like scale/complexity.
I believe the closes analogy is that Alloy is a high-level "prototype". Not in the sense that it does what real prototype will, but it models the behaviour of your prototype. It's like a proof of concept that certain thing is possible. Very new lands to me, I wonder if it's possible to apply in my web development field(or stuff like Android/iOS programming). Stuff like modeling distributed consensus is great, but that's outside of the scope for me. That example with Users, Accounts, and Resources is closer to my every day worries.
@@checkerist Ever heard of TLA+?
Can Alloy be implemented as a virtual machine for use on top of popular software platforms for direct translation into javascript python C++ and java templates?
Such tight integration would make rapid program trace and prototyping much more feasible
Alloy is just a checker, you could easily do annotations or something in most popular languages, write a tool that would build alloy models out of that and checked them.
Or you could write a tool that would generate tests from alloy models.
There is a ton of possibilities to make prototyping and programming better, but seems most people aren't interested to put time into that.
2:10 happens to me all the time! Well, not anymore, I now explain the things to myself to ensure they look consistent
Some thing which very new i learnt from this video. Thanks for sharing video.
Being a developer is a social enterprise - correctness is a social state. Most critical defects are defects in understanding, not defects in the code.
Very well said… I couldn’t agree more.
wow, i think i want alloy now
I think the solution that he doesn't give in minute 22:20 of the final example is
pred can_access(u : User , r : Resource) {
r in u.resources or some r" : Resource |
r" in r.^parent and r" in u.resources
}
instead of
pred can_access(u: User, r: Resource) {
r in u.resources or (some r.parent and r.parent in u.resources)
}
music stops at 1:15
Fantastic