Mi Sistema Operativo es un Teorema

Presenta:

L.M.A. Oscar Oswaldo Moya Pérez

Recursividad

\(f_n : \mathbb{N} -> \mathbb{N}\)

\(f_0 = 0\) y \(f_1 = 1\)

\(f_n = f_{n-1} + f_{n-2}\)

fibo :: Int -> Int

fibo 0 = 0
fibo 1 = 1

fibo n | n > 1 = fibo (n-1) + fibo (n-2)
          | otherwise 0

List Comprehension

\(C_n=\{ x\in\mathbb{N}\mid 2\leq x\leq n, x\text{ es primo}\}\)

eratosthenesCribe n = [ x | x <- [2..n], isPrime x ]

\(x\text{ es primo}\Leftrightarrow|D_x|=2\)

isPrime x = (length . factors) x == 2

\(D_k=\{ x\in\mathbb{N}\mid 1\leq x\leq k, k \ mod\ x=0\} \)

factors k = [ x | x <- [1..k], k `mod` x == 0 ]

Estructura Funcional

Types

Composition

Lazy Evaluation

fibo :: Int -> Int

isPrime :: Int -> Bool

length . factors

toSql . read . unpack

take 10 [ x | x <- [1..], isPrime x ]

Entornos Funcionales

Instala paquetes

Evalúa derivaciones

Cambia versiones manuales

Versiona todo en Git

Sobreescribe configuraciones

Reproduce entornos desde cero

nix-shell -p hello

Reproducibilidad Total

{
  description = "A Nix flake providing a Haskell development environment";
  inputs = { 
    nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.05";
    flake-parts.url = "github:hercules-ci/flake-parts";
    haskell-flake.url = "github:srid/haskell-flake";
  };
  outputs = inputs@{ self, nixpkgs, flake-parts, haskell-flake, ... }:
    flake-parts.lib.mkFlake { inherit inputs; } {
      systems = [ "x86_64-linux" ];
      imports = [ inputs.haskell-flake.flakeModule ];
      perSystem = { self', system, pkgs, ... }: { 
        haskellProjects.default = {
          basePackages = pkgs.haskell.packages.ghc96;
          devShell = {
            enable = true;
            tools = hp: { 
              inherit (hp)
              cabal-install
              haskell-language-server;
            };
          };
        };
      };
    }; 
}

{
  description = "A Nix flake providing a Haskell development environment";
  inputs = { 
    nixpkgs.follows = "haskellNix/nixpkgs-unstable";
    haskellNix.url = "github:input-output-hk/haskell.nix";
    flake-utils.url = "github:numtide/flake-utils";
  };
  outputs = inputs@{ self, nixpkgs, haskellNix, flake-utils, ... }:
    flake-utils.lib.eachSystem [ "x86_64-linux" ] (system:
      let pkgs = import nixpkgs { inherit system;
                                  overlays = [ haskellNix.overlay ];
                                };
          haskellProject = pkgs.haskell-nix.project {
            compiler-nix-name = "ghc96";
            src = ./.;
          };
          hpkgs = pkgs.haskellPackages;
      in {
        devShells.default = haskellProject.shell.overrideAttrs 
          (oldAttrs: {
            buildInputs = oldAttrs.buildInputs ++ [
              hpkgs.cabal-install
              hpkgs.haskell-language-server
            ];
          });
      }
    );
}

Sistemas FDR

{ config, pkgs, ... }:

{
  boot.loader.grub.device = "/dev/sda";
  fileSystems."/" = {
    device = "/dev/sda1";
    fsType = "ext4";
  };
  services.openssh.enable = true;
  users.users.oscar.isNormalUser = true;
  users.users.oscar.shell = pkgs.zsh;
  system.stateVersion = "25.05";
}

configuration.nix

Evaluation

Reproducible system

NixOS como estructura lógica

Servicios, usuarios, paquetes, versiones, versionado, núcleo, sistema de archivos, etc.

services.nginx.enable, environment.systemPackages, boot.kernelPackages, etc.

\(p=\{ services.nginx.enable = true,users.users.moper.isNormalUser = true,\ ...\}\)

DEFINICIONES:

Definimos 𝕊 como el espacio de estados de todos los sistemas NixOS posibles. Cada elemento 𝒙 ∈ 𝕊 representa una instancia concreta.

Definimos 𝔸 como el conjunto de todos los atributos declarables en NixOS. Cada elemento 𝒂 ∈ 𝔸 es un atributo configurable.

Decimos que 𝒑 ⊂ 𝔸 es sintácticamente consistente si no induce conflictos en el proceso de evaluación.

Un sistema 𝒙 ∈ 𝕊 satisface 𝒑 si cumple todos los atributos declarados en 𝒑, a este sistema lo llamamos modelo y denotamos con 𝒙 ⊧ 𝒑

Un teorema de consistencia

\(\exists x\in\mathbb{S}\mid x\models p\)

\(\Updownarrow\)

\(p\text{ es sintácticamente}\)
\(\text{consistente}\)

{
  description = "Oswaldo's Universal NixOS configuration";
  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs/nixos-25.05";
    nixos-wsl.url = "github:nix-community/NixOS-WSL/main";
    home-manager.url = "github:nix-community/home-manager/release-25.05";
    home-manager.inputs.nixpkgs.follows = "nixpkgs";
    flake-utils.url = "github:numtide/flake-utils";
    nixTalk.url = "github:OswaldoMoper/nixTalk";
    moper.type = "path";
    moper.path = "/home/omoper/oswaldomoper.com";
  };
  outputs = inputs@ { self, nixpkgs, nixos-wsl, flake-utils, home-manager, ... }:
  let system = "x86_64-linux";
      modules = [ nixos-wsl.nixosModules.default
                  home-manager.nixosModules.home-manager
                  (import ./nixosModules/common.nix)
                  (import ./nixosModules/graphical.nix)
                  (import ./nixosModules/webstack.nix)
                  (import ./nixosModules/postgresql.nix)
                  (import ./nixosModules/user.nix) ];
  in {
    nixosConfigurations.spartanWSL = nixpkgs.lib.nixosSystem {
      inherit system;
      specialArgs = { inherit self inputs nixpkgs nixos-wsl; };
      modules = modules ++ [ (import ./hosts/spartanWSL.nix) ];
    };
    packages.${system} = let pkgs = nixpkgs.legacyPackages.${system};
                             migrationScript = builtins.readFile ./scripts/nixos-rebuild-migration.sh;
    in { nixos-rebuild-migration = pkgs.writeShellScriptBin "nixos-rebuild-migration" migrationScript; };
    nixosModules = modules;
  };
}

Bibliografía

Halmos, P. R. (1974). Naïve set theory. Springer-Verlag.
Enderton, H. B. (2001). A mathematical introduction to logic (2ª ed.). Academic Press.
Howard, W. A. (1980). The formulas-as-types notion of construction. En J. P. Seldin & J. R. Hindley (Eds.), To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism (pp. 479–491). Academic Press.
Hutton, G. (2016). Programming in Haskell (2ª ed.). Cambridge University Press.
NixOS Foundation. (2025). Nix Reference Manual (Stable Version). https://nixos.org/manual/nix/stable
NixOS Foundation. (2025). Nixpkgs Reference Manual. https://nixos.org/manual/nixpkgs/stable
NixOS Foundation. (2025). NixOS Manual (Stable Version). https://nixos.org/manual/nixos/stable