4 ms·

The CS department at the Ohio State University built their own language on top of C++ called RESOLVE/C++. A lot of students absolutely hated it, but it introduc

The CS department at the Ohio State University built their own language on top of C++ called RESOLVE/C++. A lot of students absolutely hated it, but it introduced a pretty awesome paradigm for working with objects: swapping. If a function needs to operate on an object, rather than messing with pointers or copying the object, the function instead "swaps" the object with an initialized object. The function's "contract" specifies that it "consumes" the object that is passed in, so in code that calls that function, it is apparent that it better copy the object if it needs to access it again. I think this provides a nice paradigm for allowing for immutability without excessive copying. The only functions that actually modify objects are the object methods themselves. The RESOLVE/C++ language has been around for well over a decade, but it hasn't garnered much interest outside of academia. It's a shame, because it's a reasonably high level language that allows for mathematical proofs of correctness while still compiling down to machine code.

grav1tas 16y ago
I think with languages like Haskell, ML, Coq, ACL2 and their ilk, you're not going to get a lot of traction for theorem proving in an OOP-ed C++ variant. The first two do compile to machine code, and have type systems that better lend themselves to theorem proving. I'm not sure if C++ OOP is formal enough (or generally accepted as such) to be a strong contender in theorem proving.
daeken 16y ago
An ex-girlfriend of mine was in the CS program at OSU and I helped her out occasionally with her homework and as such spent many nights pulling my hair out and cursing the name of whomever created RESOLVE/C++. The algebraic proof side of things was so poorly documented and designed that it was effectively impossible to use for its intended purpose, and the macros for things like simple comparisons were just excruciating. I've dealt with many languages, but RESOLVE/C++ is in the elite group which I found absolutely no upside to. I really don't understand why it's still in use.
jpr 16y ago
Why not just use const references as parameters? No excessive copying, immutability. Seems like a win to me.

grav1tas 16y ago

I think with languages like Haskell, ML, Coq, ACL2 and their ilk, you're not going to get a lot of traction for theorem proving in an OOP-ed C++ variant. The first two do compile to machine code, and have type systems that better lend themselves to theorem proving. I'm not sure if C++ OOP is formal enough (or generally accepted as such) to be a strong contender in theorem proving.

daeken 16y ago

An ex-girlfriend of mine was in the CS program at OSU and I helped her out occasionally with her homework and as such spent many nights pulling my hair out and cursing the name of whomever created RESOLVE/C++. The algebraic proof side of things was so poorly documented and designed that it was effectively impossible to use for its intended purpose, and the macros for things like simple comparisons were just excruciating. I've dealt with many languages, but RESOLVE/C++ is in the elite group which I found absolutely no upside to. I really don't understand why it's still in use.

jpr 16y ago

Why not just use const references as parameters? No excessive copying, immutability. Seems like a win to me.