Hi,

my machines run on ALTLinux Sisyphus. I'm a currently inactive member of ALT Linux Team.

I'm inetersted in functional programming, logic programming, and programming with proofs in systems like Coq, Twelf, Isabelle (and also doing other tasks this way, e.g., theoretical research in maths, CS, linguistics could be published in a form supplied with Coq-like formal propositions and proofs).

I believe we need to make the computing environments more usable by going in the functional and proof-assistant direction. Nix and NixOS is a nice project and one possible step in this direction.

My dream about UI is UI based on Curry-Horward correspondence:
The UI can be like asking the system for a tool in a form of a specification (a proposition, or, equivalently, a type in a rich type-system like that of Coq), and the system assists you in finding the implementation for the wanted tool (i.e., a proof for the proposition).