|
|
|
|
|
|
by grav1tas
5541 days 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. |
|
|