[opensource] Printing files from the command line

Timothy Normand Miller millerti at cse.ohio-state.edu
Sat Feb 7 19:51:34 EST 2009


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




More information about the Opensource mailing list