[opensource] RESOLVE

Brian Swaney swaney.29 at osu.edu
Sat Feb 7 22:11:43 EST 2009


Can nobody change the subject line so it doesn't ask about Printing?

I have the opposite problem, in that I entered without knowing any 
languages. I wanted something to start with on my personal computer, but 
didn't know any languages that weren't confined to school servers 
running decade-old operating systems. It's not like I could put RESOLVE 
onto my own computer or anything.

For the record, I do support most of the RESOLVE principles. My only 2 
problems are that they are effectively wasting 3 quarters of 
undergraduates' time by denying them access to actual usable programming 
languages. For the same reason many programmers who start with .NET 
languages have difficulty with other languages such as C++, it is 
difficult to move from RESOLVE to another language if that's the only 
one you know. A more useful means of teaching the course would be to 
teach it in a language that would be useful to know.

Also, the specifications are not very readable. While I appreciate the 
need to document the input/output of your libraries, and to use the same 
"contracts" for future implementations and thusly prevent the need to 
rewrite the entire kernel for one extension, the psuedo-mathematical 
syntax used is often less readable than the code itself. If they want us 
to use their style, they should make a point of how it simplifies 
programming by making their documentation readable. I claim this can be 
done without losing preciseness if done carefully, and is much easier. 
The current specifications actually (for me) make RESOLVE harder, but 
maybe that's just me. I've left feedback multiple times, both verbally, 
and in course evaluation forms, but I get the feeling that the RSRG is 
closed-minded on how they teach the series.


-Brian Swaney



Silas Baronda wrote:
> Resolve/C++ is fine for what they need it to do. If you come into the 
> class not knowing any other language then this is all good.  My 
> problem was that I came in and I knew about c, python, php, etc and 
> was not trying to think like deeply about the subject taught.  I 
> considered it basic classes about another language and wanting to get 
> through as quickly as possible so I can take better/cooler classes.  I 
> actually never thought they would go this deep in the early CSE classes.
>
> Now if someone came into this program not knowing any prior language 
> then I think they would concentrate more on the things taught as a 
> subject instead of the language.  They wouldn't think of the language 
> as the constraint but the actual problem they are trying to solve.
>
> I vote for objective-c as the language for the sequence. Just j/king
> On Feb 7, 2009, at 7:51 PM, Timothy Normand Miller wrote:
>
>> As I understand it (knowing Bruce Weide and some of his RAs), Resolve 
>> C++ is basically C++ with Resolve concepts layered on top of it.  
>> There is, in fact, a "pure" Resolve language that they use in their 
>> software verification research.  This language has quite a different 
>> syntax and is more abstract and "academic" in nature, although they 
>> have an interpreter for it.  The pure Resolve language also provides 
>> a means to add logical specifications that describe the meaning of 
>> what your algorithm is supposed to implement.  They're actively 
>> researching using automatic theorem provers to determine whether or 
>> not your algorithm is consistent with the logical constraints (or 
>> vice versa).  While I'm not a fan of massively type-strict languages 
>> and such (Pascal, Ada, VHDL, etc.), I can definitely see the value in 
>> having a system for PROVING that your code is correct according to 
>> its specification.
>>
>> They use Resolve (C++ or not) to teach high-level language concepts 
>> that can be implemented in any language, but their goal is to 
>> abstract away a lot of the mechanics of programming and focus on 
>> those concepts.  Stacks, queues, algorithms, logical constraints, etc.
>>
>> Personally, I think that if one were to select a mainstream language 
>> to use to teach these things, something purely OO like Ruby (or 
>> perhaps Python) would be better than Java, if only for the lack of 
>> legacy cruft and simpler syntax that don't distract from the concept 
>> being explored.
>>
>> Of course, if you want an interesting challenge, you should try doing 
>> all of this stuff in Verilog or VHDL.   :)
>>
>>
>> On Feb 7, 2009, at 6:25 PM, Paul Betts wrote:
>>
>>> Why am I only on my phone when good mails like this show up?
>>>
>>> Anyway, short summary is, Resolve is great ideas hampered by a crap 
>>> language (C++) that really clouds the solid underlying concepts.
>>>
>>> -- 
>>> Paul Betts
>>>
>>> On Feb 7, 2009, at 14:46, Shaun Rowland <rowland at cse.ohio-state.edu> 
>>> wrote:
>>>
>>>>
>>>> On Feb 7, 2009, at 2:25 PM, Aaron Joseph wrote:
>>>>>
>>>>> Also, I never asked anyone to send me the key, I just wondered if 
>>>>> someone has successfully gotten it from soc lab or oit or some 
>>>>> other legal source. And it seems like the answer is that no-one 
>>>>> like soc lab or oit has it for free.
>>>>
>>>> That is a little much to infer from what was stated. I am not going
>>>> to dwell on this. I gave my nudge about the subject.
>>>>
>>>>> Shaun, no-one is going to think you're "the man" for trying to do 
>>>>> what's right. However you could have helped me out a little when I 
>>>>> was trying to argue why RESOLVE sucks at that UG forum!
>>>>
>>>> :-)
>>>>
>>>> Heh. I really don't want to start a big discussion about Resolve.
>>>> But I can't resist giving my current impression - at least a little.
>>>> It is impossible to broach the subject without writing a book.
>>>> I have seen this argument come up so many times over the years.
>>>> I knew C++ pretty well when I came into Resolve. I also used to
>>>> wonder if it might be better to use another language which would
>>>> have given me more practical experience. I can't remember how many
>>>> of the things we learned there I had picked up reading on my own
>>>> (that's pretty much how I learn for the most part), but I've
>>>> always wondered if knowing a certain amount enabled me to fly
>>>> through those courses while not having all the material sink
>>>> in as much as it could have. I am not really worried about that
>>>> now. I have a lot more experience than back then. Learning to use
>>>> a new programming language is not a big deal IMO. That's more
>>>> of a practical concern which I prefer to do on my own anyway.
>>>> The "practical" side of the argument is greatly outweighed by
>>>> the "learning the concepts" side - especially now that I am
>>>> older.
>>>>
>>>> One of my problems when I was taking undergrad courses was
>>>> that I was more interested in doing things on my own instead
>>>> of doing homework... but that's another story. I am sure I'd
>>>> still have that problem, but I hope I am more disciplined now,
>>>> however it just might be hopeless :-)
>>>>
>>>> Anyway, Bruce is co-director of the CSE department's Reusable
>>>> Software Research Group. He's a really smart guy. I'm sure that's
>>>> an understatement. Even if I wanted to argue about Resolve, I'd
>>>> put a _lot_ of thought into it first, probably come to the
>>>> conclusion that I'm possibly missing something that someone
>>>> who is an expert in the field knows, and then spend a lot
>>>> more time investigating it. Maybe if I wanted to argue about
>>>> it I'd end up learning even more reasons why the course sequence
>>>> is a good idea as is. Actually, I already feel that's the
>>>> case. The arguments for it being the way it is seem sound to
>>>> me. Bruce cares a lot about teaching. I am sure he's thought
>>>> about this much more than anyone else here, and he knows what
>>>> he's doing. I'm not saying that because he's a faculty member
>>>> of the department in which I work either.
>>>>
>>>> If one is worried about this being a main item on their resume
>>>> and people wondering what it is, I don't see that as an argument.
>>>> It is good to not discuss the fact it was Resolve, but what you
>>>> have learned in the sequence. Besides, you'll probably have
>>>> time to learn "resume enhancing" languages before you're resume
>>>> would depend on such factors anyway. Once you know the art of
>>>> programming, picking up a "practical" language is not a big
>>>> deal I think. I've seen the Resolve argument come up over
>>>> the years, and the "practical language" argument means nothing
>>>> to me at this point.
>>>>
>>>> So, my short answer is that I think the Resolve sequence is
>>>> fine - so if I spoke up, I'd end up being on the wrong side
>>>> of your battle :-)
>>>>
>>>> I'll give you one seemingly supportive argument about how
>>>> I was annoyed in a group project once when two of us
>>>> wanted to use C++ and the other two said they knew real
>>>> C++ and not just Resolve... and they didn't, so it was
>>>> annoying. There are reasons why this experience was silly
>>>> however: a) Why would I ever have wanted to use C++?
>>>> b) Either language would not have made a big difference.
>>>> c) These group projects annoy me because I am a pain
>>>> to program with, caring about using white space correctly,
>>>> caring about things like using private data instead of
>>>> just making everything public (some people miss the point),
>>>> and planning out design first... using revision control.
>>>> d) It really had absolutely nothing to do with Resolve
>>>> itself. See, on the surface it seems supportive, but it
>>>> isn't :-)
>>>>
>>>> I know this is all extremely way off topic. I'm bored right
>>>> now.
>>>> -- 
>>>> Shaun Rowland
>>>> rowland at cse.ohio-state.edu
>>>>
>>>>
>>>>
>>>> _______________________________________________
>>>> Opensource mailing list
>>>> Opensource at cse.ohio-state.edu
>>>> http://mail.cse.ohio-state.edu/mailman/listinfo/opensource
>>> _______________________________________________
>>> Opensource mailing list
>>> Opensource at cse.ohio-state.edu
>>> http://mail.cse.ohio-state.edu/mailman/listinfo/opensource
>>>
>>
>> Timothy Normand Miller
>> millerti at cse.ohio-state.edu
>> http://www.cse.ohio-state.edu/~millerti
>>
>>
>> _______________________________________________
>> Opensource mailing list
>> Opensource at cse.ohio-state.edu
>> http://mail.cse.ohio-state.edu/mailman/listinfo/opensource
>
> _______________________________________________
> Opensource mailing list
> Opensource at cse.ohio-state.edu
> http://mail.cse.ohio-state.edu/mailman/listinfo/opensource
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/x-pkcs7-signature
Size: 3237 bytes
Desc: S/MIME Cryptographic Signature
Url : http://mail.cse.ohio-state.edu/mailman/private/opensource/attachments/20090207/fb37f5de/smime-0001.bin


More information about the Opensource mailing list