scscsc

When you want to check whether A >= B (where A and B are numbers represented as floats), you would probably want to use the check A >= B - epsilon.

There is a stronger system, called "intuitionistic propositional logic", where this axiom is not valid. There are less formulae that are valid intuitionistically, but any formula that is valid intuitionistically is also valid clasically.

There are various philosophical reasons why one prefers intuitionistic logic, but note that in any case it is stronger to have an intuitionistic proof, so these are preferable (when they exist).

"With the advent of what is called "large scale integration" (being a term from the computer field, its acronym LSI is better known!) it seems to become technically feasible to build machines more like "clouds of arithmetic units" with information processing activities going on simultaneously all over the place, for shorter periods of time even independently of each other. Programming for such machines will pose completely different trade-off problems: one will be willing to invest in potentially useful computing activity before its actual usefulness has been established, all for the sake of speeding up the whole computation. But although I know such machines may be coming, I shall not touch these problems for the following reasons. First, as far as general purpose applications are concerned, I have my doubts about the effectiveness with which such forms of parallelism can ever be exploited. Second —and that is the most important consideration— parallel programming is an order of magnitude more difficult than sequential programming."

Also, the first mention of "cloud", although with a different meaning.

This style of working is needed in large code bases, where not all files are checked out on developer workstations (for performance or privacy reasons).

By far, the most interesting part is automatically generating the levels by difficulty. In my implementation, I first generate a full puzzle and then start removing pieces one by one, as long as the part just removed can be logically deduced. The only difference between easy/medium/hard is the amount of work performed in the logical deduction: one step for easy, two steps for medium and three for hard.

http://mipmemorial.blogspot.ro/p/cheers-to-mihai.html

I find it funny that nowhere on the official page (code.visualstudio.com) does it say that it's an editor.

Has your client ever reported a bug?

Was it a bug you cared about?

Why haven't you discovered it during testing?

c_i is the i'th version of the compiler.

    c1 c2 // c1 compiles c2

    c2 c3 // c2 compiles c3

But apparently there is no better thing to do.

There is always a disconnect between what you mean and what you say. It happens all the time and the risk is not going to go away. People who work with proof assistants understand this risk better and most of them are pretty happy that the risk is sufficiently small for their purposes.

However, this is mitigated by having only a very small core that checks the proofs. Basically if there if a wrong proof goes through, there must be an error in the core (which was checked by many people and is very small).

Is the solution unique to each puzzle?

The style is similar to my game NoThree for Android (https://play.google.com/store/apps/details?id=com.ovaludi.no...).

I was curios if anyone here is mining bitcoins and if it's worth their time.

Object-orientation sucks for everything except user interfaces. If you don't believe me, try writing a UI library without objects and see what happens. UI is OOP's best (and only compelling) use case.

For all other algorithms classical data structures/ADTs are much better. If you don't believe me, try writing an OOP compiler.

I've been working (and still am) on an Android puzzle game using libgdx. The puzzle requires to fill a board with Xs and Os while obeying the no-three rule (no three Xs or Os in a row) and the same number rule (same number of Xs and Os on each line and column).

The puzzle turned out to be quite challenging and addictive, similar to sudoku. The most difficult part of development was that I would start the game to see check a new feature and I wouldn't get back to development until I finished filling the board.

The most interesting part of development was writing the algorithm that generates the board in order to ensure a unique solution and account for the various levels of difficulty.

I've already published a version of the game and I'm currently working on adding some features to it.

    node *remove_if(node *head, remove_fn rm)
    {
        if (rm(head)) {
            return remove_if(head->next);
        }
        head->next = remove_if(head->next);
        return head;
     }

    #define max(a, b) ((a) > (b) ? (a) : (b))
    #define geth(n) (n->h = 1 + max(n->l->h, n->r->h))
     
    struct node
    {
          int key, h;
          struct node *l, *r;
    } *R, *NIL;
    typedef struct node node;
     
    void init(void)
    {
          R = NIL = (node *) malloc(sizeof(node));
          NIL->key = NIL->h = 0,
                  NIL->l = NIL->r = NULL;
    }
     
    node* rotleft(node *n)
    {
          node *t = n->l;
     
          n->l = t->r, t->r = n,
                  geth(n), geth(t);
          return t;
    }
     
    node* rotright(node *n)
    {
          node *t = n->r;
      
          n->r = t->l, t->l = n,
                  geth(n), geth(t);
          return t;
    }
     
    node* balance(node *n)
    {
          geth(n);
          if (n->l->h > n->r->h + 1)
          {
                  if (n->l->r->h > n->l->l->h)
                          n->l = rotright(n->l);
                  n = rotleft(n);
          }
          else
                  if (n->r->h > n->l->h + 1)
                  {
                          if (n->r->l->h > n->r->r->h)
                                  n->r = rotleft(n->r);
                          n = rotright(n);
                  }
          return n;
    }
     
    node* insert(node *n, int key)
    {
          if (n == NIL)
          {
                  n = (node *) malloc(sizeof(node));
                  n->key = key, n->h = 1, n->l = n->r = NIL;
                  return n;
          }
          if (key < n->key)
                  n->l = insert(n->l, key);
          else
                  n->r = insert(n->r, key);
          return balance(n);
    }
     
    node* erase(node *n, int key)
    {
          node *t;
          if (n == NIL) return n;
          if (n->key == key)
          {
                  if (n->l == NIL || n->r == NIL)
                  {
                          t = n->l == NIL ? n->r : n->l;
                          free(n); return t;
                  }
                  else
                  {
                          for (t = n->r; t->l != NIL; t = t->l);
                          n->key = t->key,
                                  n->r = erase(n->r, t->key);
                          return balance(n);
                  }
          }
          if (key < n->key)
                  n->l = erase(n->l, key);
          else
                  n->r = erase(n->r, key);
          return balance(n);
    }
     
    int search(node *n, int key)
    {
          if (n == NIL) return 0;
          if (n->key == key) return 1;
          if (key < n->key)
                  return search(n->l, key);
          else
                  return search(n->r, key);
    }