rationalskepticism.org

mizvekov wrote:Well, there is a lot of people out there really pumped with all this new stuff, and if you look around, say for instance in github, you will see the place is choke-full of people creating new libs that solve problems already handled by well established ones, except that by doing it the c++11 way. Some of it is promising, some of it looks like shit, but it's only wait and see now.
About the old libraries, well that varies a lot. There has not been a lot of time since the spec got published, and there is no fully conformant compiler / STL implementation yet. Lot's of libraries in boost for instance have been updated to accept and work well with the new additions, but there are still rough edges and not every new feature has been exploited yet.
But still you have got other libraries like Qt which are still using pretty ancient c++ lingo, and still uses that infamous preprocessor called 'moc', for things that could be done just using the standard lib. I've read on their mailing list that they have committed themselves to supporting at least the new stuff which only requires superficial changes and which can be optional, but I guess they still have to support ancient platforms with no hope of ever seeing a c++11 compliant compiler, so I venture to say that no radical changes in the API are to be expected for years to come. Plus their codebase is pretty huge...

Interesting. I thought that GTK was the C library and Qt very much the modern C++ library. I suppose they've been around long enough to both be "outdated" in their own ways.

Though since using languages outside the C family, I've come to appreciate technologies like GTK and OpenGL, which use such simple C code that they become almost trivial to bind to from other languages.

VazScep wrote:Yes, but the Java guys haven't been always successful at that. Last I checked, their GUI situation was a mess, with AWT, swing, SWT etc still competing. But then looking at that side, the other languages do not fare better, except perhaps C#.

Ugh. No fucking idea, but you might well be right about Java's GUI situation. But I'm not sure Microsoft is doing any better. While looking into GUI development on Windows, I was put off by how quickly Microsoft moved from Windows Forms to Windows Presentation Foundation, and by rumours that Microsoft might be ditching Silverlight and moving to Javascript, and then with their rehaul of the look and feel of their widgets with Windows 8. I've read numerous concerns from developers saying "what does Microsoft want us to use?"

GUIs to me seem like a problem that no-one in the software industry has ever really figured out, possibly because a user's expectations of a GUI aren't particularly amenable to precise engineering. I'm only messing around with GUIs as part of a hobby project, and I'm doing it in Ocaml using the Ocsigen framework, which has so far blown me away. But even their framework has yet to commit on using callbacks for event handling or to go with the more declarative reactive frameworks.

VazScep wrote:Well, to be 'fair' to them, that was their introductory course to programming, but you would rarely see it again later in the course. I don't think any of the professors had a vested interest in it, I don't remember seeing anything being published on the matter.

Ah, okay. It would probably vary with the universities anyway. Being at Edinburgh, ML and Haskell are a pretty big deal. Phil Wadler's the professor of computer science here, a position once held by Robin Milner.

Well, if you're interested at all in formal logic, the original inspiration for ML and its earliest applications (such as Logic of Computable Functions) are still, IMO, some of the smartest and coolest examples of functional programming engineering and awesome uses of type abstraction and higher-order functions. I can throw some simple Haskell code your way if you're interested.

Sure I am, thanks

Cool. Well, I don't know if I'm going to be able to explain it very well. But here's the most basic idea. Suppose you want to prove stuff in propositional logic. You could do this by writing a SAT solver, but this has a few drawbacks: firstly, the code is probably going to be very complicated, and there's every chance it will contain the odd bug, which is useless for mission-critical verification; secondly, it's not going to scale to logics which are undecidable, such as first-order logic. So you instead work from axiomatics. It turns out that everything in propositional logic can be proven by instantiating the following axioms, and applying modus ponens appropriately:

1) P -> (Q -> P)
2) (P -> Q -> R) -> (P -> Q) -> (P -> R)
3) (~P -> ~Q) -> (Q -> P)

You can code this up as follows:

Code: Select all

-- An encapsulated logical kernel for a Hilbert-style Propositional Calculus

module Propositional (Theorem, Term(..), axiom1, axiom2, axiom3, mp, instTerm, inst,
                      theoremTerm) where

infixr 8 :=>:

data Term a = Var a
            | Term a :=>: Term a
            | Not (Term a)
            deriving (Show,Eq,Ord)

newtype Theorem a = Theorem (Term a) deriving (Eq, Ord, Show)

theoremTerm :: Theorem a -> Term a
theoremTerm (Theorem t) = t

(p,q,r) = (Var "p",Var "q",Var "r")

axiom1 :: Theorem String
axiom1 = Theorem (p :=>: q :=>: p)

axiom2 :: Theorem String
axiom2 = Theorem ((p :=>: q :=>: r) :=>: (p :=>: q) :=>: (p :=>: r))

axiom3 :: Theorem String
axiom3 = Theorem ((Not p :=>: Not q) :=>: q :=>: p)

mp :: Eq a => Theorem a -> Theorem a -> [Theorem a]
mp (Theorem (p :=>: q)) (Theorem p') = [Theorem q | p == p']
                                                 
instTerm :: (a -> Term b) -> Term a -> Term b
instTerm f (Var p)    = f p
instTerm f (Not t)    = Not (instTerm f t)
instTerm f (a :=>: c) = instTerm f a :=>: instTerm f c

inst :: (a -> Term b) -> Theorem a -> Theorem b
inst f (Theorem t) = Theorem (instTerm f t)

Here, the syntax of propositional logic is captured by a simple data-type. The theorems are encapsulated as a type "Theorem" whose data constructors we do not export. Thus, the only theorems that clients can construct are "axiom1", "axiom2", "axiom3"; instantiations of the form "instTerm f thm"; and theorems resulting from modus ponens. It is impossible for a client to ever construct a theorem such as "p -> ~p", since this is not a tautology. The only theorems that can be constructed are precisely the theorems of propositional logic.

This is called a "logical kernel" and the advantage of it is that it is made up of very little code and it is easy to verify as bug-free (there isn't even a single loop to consider). So the security of the code here is very secure. You can be sure that clients cannot use this code in ways to generate non-theorems.

On top of this, you wrap a whole load of additional functionality, probably culminating in a complete tautology-checker. But the great thing about the tautology-checker is that its outputs are guaranteed correct with respect to the kernel. The tautology checker would probably input a Term, and if the term is a tautology, it would output a Theorem. And since the only ways to construct theorems are to apply the rules of kernel, you can be absolutely sure that if it does output a theorem, that theorem really is a tautology.

This is just the beginning. The design of the proof tools you build on top are something else.