More code = more hackable

Software gets more and more bloated.

How are you supposed to secure Linux when it has a billion unnecessary features? You set up a Linux VPS, and you think of maybe a few things you need to secure, while forgetting about everything else, because it has so many lines of code and so many features that you don't even know all of what it's doing. Knowing how to use command line tools and shell scripts and basic Linux/Unix skills doesn't mean you know every single file or process running on it. It's too complex.

The same is true for any other software, especially if it uses user input or does something over a network.

Applying a security patch doesn't solve the issue of code sprawl, scope creep, etc. Bloat isn't just about performance, but also security. If you continue to add more and more shit to a project, even if that shit is security patches, it will become unmanageable, and over time, it becomes harder and harder to secure, like with PHP or Flash, which is part of why they're dying. You have to refactor and gut out legacy shit, making the same functionality have a smaller code base, making sure it's properly documented (and that the documentation is up to date! comments don't matter if they're obsolete), and getting rid of features that you can't secure properly.

Unfortunately, however, everything we use is getting more and more bloated, and it isn't showing any signs of stopping. We're building flawed code on top of flawed code. Websites made with flawed stacks. Making higher-level languages built on top of hard-to-secure lower level languages which lack proper memory safety features, among other things.

We're at the point where, you can know just a couple dozen security vulnerability categories, and you can hack so much shit -- simply because we're too incompetent to even get rid of well-known categories of vulnerabilities. Legacy code building on legacy code, and it's garbage all the way down.

What will it take for people to scrap what we have and start from the ground up with more security features in mind? I'm talking new network protocols, new operating systems, new web stacks, new everything.

We are building a high-tech future of smart and IoT bullshit that is trivially easy to hack. We are building driverless cars that are gonna get owned on day one. We are designing AI and robots and shit to dictate our future, but who in their right minds thinks this is a good idea when everything is hackable as fuck?

This is why we need dependent types.

That's the point of microkernels. You only pull in the parts of the OS that you actually need, so the stack remains small enough that you can actually read and understand it all yourself.

>>2
redpill me on dependent types
>>3
how come nobody uses minix then?

>>4
Basically you can have functions that take values and return types, such as
f : forall x : Nat. *
f 0 = Bool
f _ = Nat

So you can do a lot of fun stuff like
g : forall x : Nat. f x
g 0 = False
g _ = 0

The safety comes from the fact that type constructors are also functions and thus can also depend on values, consider
Vect : forall n : Nat. forall t : *. *
Cons : forall n : Nat. forall t : *. forall v : Vect n t. Vect (Succ n) t
Nil : forall t : *. Vect 0 t

Say that you make the functions head and tail for the above vector construction thing, their types would be like:
head : forall n : Nat. forall t : *. forall v : Vect (Succ n) t. t
tail : forall n : Nat. forall t : *. forall v : Vect (Succ n) t. Vect n t

If you try to do head 0 Nat (Nil Nat) the compiler will scream at you as the type of Nil Nat is Vect 0 Nat while head 0 Nat next expects a value of type Vect (Succ 0) Nat, and these two do not match.

You can do more fun stuff with it, such as type-safe printf: https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c115292

Cons : forall n : Nat. forall t : *. forall v : Vect n t. Vect (Succ n) t

*Cons : forall n : Nat. forall t : *. forall a : t. forall v : Vect n t. Vect (Succ n) t

>>4
Please respond, it took me 90 days to write these ;_;

>>7
a