Davidbrcz

The idea is to write the spec (is grammar and semantics) only once and have for free a compiler as well as some formal tools (model checker,...)

C had been formalized with it for instance.

Very convenient. I have used it for ROS projects with multiples SCM

A simple button for scanning a document, the software does all the processing for you (rotation, OCR,..). You can apply tags to documents, search them, export them. The storage format is more than open (a png file + OCR results as an HTML page,...)

    Reversing: Secrets of Reverse Engineering de Eldad Eilam
    Practical Reverse Engineering: x86, x64, ARM, Windows Kernel, Reversing Tools, and Obfuscation de Bruce Dang, Alexandre Gazet, Elias Bachaalany, Sébastien Josse
    Cryptography Engineering de Niels Ferguson, Bruce Schneier, Tadayoshi Kohno
    Applied Cryptography: Protocols, Algorithms and Source Code in C de Bruce Schneier

CMake has its drawbacks, fair enough, but 10 years ago it was pretty much already the de facto standard build system for C++. What would have used instead of CMake ?

  - Make and autotools (Haha) ? 
  - scons ?
  - completely custom build system ?
  - something else ?

Otherwise, I have been personally using ROS for building robots for the French (and European) robot championship (see https://twitter.com/AIGRIS_Birds). It works pretty well, it is convenient, easy to learn and provide some nice tooling (bagging for replaying messages, simulation with Gazebo...).

It is the de facto standard for robotics middleware for scientific projects. It not widely used by industrials because of some shortcomings even if initiatives like ROS Industrial and ROS 2 will likely improve things.

Also, JPL released its model-checker Java PathFinder and hosts every year the Nasa Formal Method conference so I'm pretty confident that at least someone at NASA is interested in formal methods =)

Formal verification has been around for 40/50 years and we can't say it is a wide success from a industrial point of view. It has some achievements in terms of results/methods and projects checked, but on a daily basis, pretty much no one uses it. We are ages away of having every programmer understanding formal verification and having all programs verified/proved.

Type theory is in a similar situation. Many issues in code could be solved with basic typing algorithms but people and companies favor languages with poor/no typing (python, Javascript).

  Deft is an Emacs mode for quickly browsing, filtering, and editing directories of plain text notes, inspired by Notational Velocity. 
  It was designed for increased productivity when writing and taking notes by making it fast and simple to find the right file at the right time and by automating many of the usual tasks such as creating new files and saving files.

Ring is a free and universal communication platform which preserves the users' privacy and freedoms.

    Official GNU package
    Released under GPLv3 licence
    Supported by an active community

    OpenDHT protocol
    Decentralized communication
    Peer-to-peer discovery and connection

    End-to-end encryption with authentification
    Identity managed by X.509 certificates
    Based on RSA/AES/DTLS/SRTP technologies

Any lisp (Scheme, Closure...)

Prolog: logic programming. Tell the computer what you know, ask a question and let it compute the answer for you.

The worst is that it will cost tax payers millions

If they want to travel, they need to be completely off and you can grant it to some people.

If they want to work on some side project, then say no to some of them but propose a part-time job (work 2 or 3 days a week). Make sure to explain why you are saying no (can not afford to give half the staff a year off).

The idea is that you have a maybe object that is either an just an object (denoted Just(a)) or nothing at all (denoted Nothing). If you want to manually apply a function f on object m, the code would look like this

  if(m is Just(a)){
      f(a)
  } else{
       // there is nothing to do
  }

  apply(m,f){
    if(m is Just(a)){
         return Just(f(a))
    } else{
         return Nothing.
    }
  }

  apply(apply(apply(m,f),g),h)

  do
    m <- getData
    b <- f a
    c <- g b
    d <- h c
    print d

I hope it helps =)

I'm just pointing out that comparing only raw figures is not relevant.

I've been running it for a while on a VPS I rent. I provides file sync, calendar, audio player, password storage (passman), weather and much more with many plugins (which are really easy to install with the app store).

It's stable and the biggest hurdles I have encountered were linked to mysql and charset encoding that lead to something to be above the maximal value in the database.

You may also want to try freelance. It is hard as you need to find clients but you are you own boss and pick whatever job you want.

Depending on your education, you could try to join a laboratory as a research associate.