My dirty secret as a computer scientist is that I’m terrible at writing and reading proofs. This interactive tutorial on the Sequent Calculus was the first time that I could do anything useful and it helped me a great deal.
Here’s the thing I always wonder about: is there anything I could actually use this for in daily practice? All the examples are always either trivial or abstract (or both). Have you ever used something like this to solve a nontrivial, but concrete, problem to e.g. simplify a program? Where simple boolean arithmetic, perhaps with a truth table thrown in, didn’t cut it?
So to be honest, I have used Alloy for much of this. More than any theorem prover, the specification capability was most beneficial. At this juncture, anyone would be remiss not to point out Hillel Wayne and his excellent work in this area.
For a gentle introduction to formal reasoning, I would strongly recommend looking at ACL2s and the undergraduate course based on it. It comes with a reasonable eclipse support.
I was a TA for this course few years back and it was interesting to see student with basic programming knowledge and no formal methods background use the tool in a very fruitful way. Of course, for more advanced usage, there has been a multiple decades of work in the industry and academics with ACL2 (theorem proved on which ACL2s is based on).
Definitely I didn’t think it through. Of course someone comes to ask what I tried to do, or what was the point.
I’ve tried to get a cache of posts for slow weeks, but they aren’t that good as what is produced when I’m just writing something every weekend.
The point was to explain, but also had this discussion and I think I half-misunderstood what he said because he was not being clear about it. But the way I understood it, I realized I had thought that way before.
It was also written in slight anger. But decided to share the link because this opens up an opportunity for people to rip up me a new if I’m wrong about an important subject. I could still be if nobody proceeds, but.. :)
Well it’s hard to know if you’re wrong or not when the point is unclear. To correct mistakes I would first have to understand what you’re trying to say.
Did read it through. I noticed what you mean. The text is not consistent in whole. I did screw it up.
No easy way to fix and it’d be a different post in the end. I’ll try to write a better version of this in future. The individual pieces seem ok though. For now I guess it can be read but if you do, don’t worry about what the text in whole tries to say.
If you come up with actionable proposals on how to improve my texts, I could apply those. Otherwise dunno. I think there’s something but I find it very hard to get.
It doesn’t work that way. To get people’s attention, you have to come up with stuff that they find worthwhile and/or accurate depending on the goal. It has to be targeted to the right audience, too. Your numbered points told me you understand some of the benefits. I wasn’t sure about a lot of the rest. I figured it was you sharing your moment by moment thinking as you later told us. Brave, but not easy to learn from.
You might want to just continue exploring this stuff to understand it more thoroughly. It’s quite complex, pretty deep, and very unnatural. Especially, if you’re not a mathematician. Keep digging into it and talking to people that understand it until you know you really get it or some part of it. Then, figure out how to share that and/or build on it. Best I can tell you since I don’t get most of it at any deep level. :)
My dirty secret as a computer scientist is that I’m terrible at writing and reading proofs. This interactive tutorial on the Sequent Calculus was the first time that I could do anything useful and it helped me a great deal.
Nice, thanks for the link.
Here’s the thing I always wonder about: is there anything I could actually use this for in daily practice? All the examples are always either trivial or abstract (or both). Have you ever used something like this to solve a nontrivial, but concrete, problem to e.g. simplify a program? Where simple boolean arithmetic, perhaps with a truth table thrown in, didn’t cut it?
So to be honest, I have used Alloy for much of this. More than any theorem prover, the specification capability was most beneficial. At this juncture, anyone would be remiss not to point out Hillel Wayne and his excellent work in this area.
For a gentle introduction to formal reasoning, I would strongly recommend looking at ACL2s and the undergraduate course based on it. It comes with a reasonable eclipse support.
I was a TA for this course few years back and it was interesting to see student with basic programming knowledge and no formal methods background use the tool in a very fruitful way. Of course, for more advanced usage, there has been a multiple decades of work in the industry and academics with ACL2 (theorem proved on which ACL2s is based on).
I’m confused about the point of the article. Why is the tone so confrontational if the point is to “explain”?
Definitely I didn’t think it through. Of course someone comes to ask what I tried to do, or what was the point.
I’ve tried to get a cache of posts for slow weeks, but they aren’t that good as what is produced when I’m just writing something every weekend.
The point was to explain, but also had this discussion and I think I half-misunderstood what he said because he was not being clear about it. But the way I understood it, I realized I had thought that way before.
It was also written in slight anger. But decided to share the link because this opens up an opportunity for people to rip up me a new if I’m wrong about an important subject. I could still be if nobody proceeds, but.. :)
Well it’s hard to know if you’re wrong or not when the point is unclear. To correct mistakes I would first have to understand what you’re trying to say.
Did read it through. I noticed what you mean. The text is not consistent in whole. I did screw it up.
No easy way to fix and it’d be a different post in the end. I’ll try to write a better version of this in future. The individual pieces seem ok though. For now I guess it can be read but if you do, don’t worry about what the text in whole tries to say.
If you come up with actionable proposals on how to improve my texts, I could apply those. Otherwise dunno. I think there’s something but I find it very hard to get.
It doesn’t work that way. To get people’s attention, you have to come up with stuff that they find worthwhile and/or accurate depending on the goal. It has to be targeted to the right audience, too. Your numbered points told me you understand some of the benefits. I wasn’t sure about a lot of the rest. I figured it was you sharing your moment by moment thinking as you later told us. Brave, but not easy to learn from.
You might want to just continue exploring this stuff to understand it more thoroughly. It’s quite complex, pretty deep, and very unnatural. Especially, if you’re not a mathematician. Keep digging into it and talking to people that understand it until you know you really get it or some part of it. Then, figure out how to share that and/or build on it. Best I can tell you since I don’t get most of it at any deep level. :)