CMCDragonkai

Purely functional programming, Logic programming and Theorem proving

The 3 axes of purely functional programming, logic programming and theorem proving are interrelated. It could be imagined that for each language listed below, they have a radar chart on all 3 axes, representing strengths and weaknesses. There's also a 4th axis for those concerned about non-programming language theory, that could be called "practicality", the ability to use it for practical engineering tasks. Finally there's a common theme between all 3 axes, which is "dependent typing".

• Coq - theorem proving
• Idris - functional programming and theorem proving
• Agda - functional programming and theorem proving
• Twelf - logic programming and theorem proving
• Prolog - logic programming

alexpana

Various 'features' of C++ that show the hacky / inconsistent way in which the language was constructed. This is a work in progress, and currently contains some of the reasons I can remember why I've given up on C++. If you want to contribute, leave your favourite "hack" in the comments.

1. (in)Visibility: C++ allows changing the access modifier of a virtual function in the derived class. Not only does C++ have no notion of interfaces, it actually allows subclasses to hide methods declared public in the superclass.

2. Operator over-overloading: One of the increment operators takes a dummy int parameter in order to allow overloading. Can you tell which without googling? (hint: its postfix).

3. Exception unspecifiers: C++ has two types of exception specifiers: throw() and nothrow. The first is deprecated (because 'we screwed up, sorry, let's forget about this terrible mess'). The second one guarantees it's contract by terminating the application when violated. That's because functions declared