Typical Free Software fanatic

Linux radical attempts to use modern web framework and cannot get past a hello-world because he keeps diving into the internals.
https://medium.com/@mattholt/its-2019-and-i-still-make-websites-with-my-bare-hands-73d4eec6b7

This article is pissing me off, cause I write websights like this yet demand no fanfare.

>>2
It's because you're not building your identity based on obnoxiously being unwilling to learn.

>>3
*willful to learn.

Proof equality in some dependent type theories such as CoC do not care about the internals. All proofs of a certain proposition are equal, same for different proofs between equal propositions. This clearly shows that internals do not actually matter in such dependent type theories. Heck, internals do not even matter in type theories with universes (where different proofs of the same proposition are not necessarily equal) - if you do not have typecase all proofs of the proposition (t : *) -> t -> t are equal for example.

Dependent types are what we need in order to ignore the internals and focus on what matters.

golang user

opinion discarded

brainlet posing as some sort of hacker