We don’t do anything like this in Australia. I can’t imagine being forced every morning to pledge something you’re not old enough to understand.
469 karma · joined September 14, 2017
I don't want to make it seem like I'm proving anything novel here, the proof I work through is definitely pretty basic as far as proofs go. It's written somewhat narratively because it reflects a train of thought I went through a few days ago when reading about existential types in Rust. Seeing the theorem ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) in the blog post made me want see if I still remembered enough Coq to prove it, and then when I was sitting down this morning to write something I thought it would make a good blog post as it explores some deep cuts of what I've been learning in Rust and might make a good introduction for people into Coq. I'll definitely take it on the chin that I titled the blog too ambitiously however and I'll be more modest with my titles in the future.
What would you have titled the blog instead to be less misleading?
However no type system of a Turing complete programming language can ever be truly trusted as a proof system because looping forever or other non-termination can be used to prove any proposition.
const proveAnything = <A>(): A => proveAnything()
However, take Rust's ownership system for example, it uses a type system that corresponds to a kind of logic called a sub-structural logic that denies one of the axioms of typical classical logic systems, namely, the weakening axiom, e.g. a function of the type
fn <A>(a: A) -> (A, A) { ... }
It’s a shame that more engineers don’t have the time or interest to learn formal verification because it’s really enjoyable once you get the hang of it. Although it rarely directly comes up at work, I think it gives a good framework for thinking in strongly types languages with advanced type systems like Rust, Typescript, or Haskell.
type Bar interface {
BarMethod(int, int) int
}
type Foo struct {}
// Error: Foo does not implement Bar (missing method BarMethod)
var _fooImplementsBar Bar = Foo{}The introduction of generics should make it easier to wrap these lower level concurrency primitives into higher level safe constructs without needing code generation or runtime type casting via interface{}.
Most devs also struggle to structure go programs in a way that makes them easily testable, but that’s true in a lot of languages.
If Facebook wants to be the “town square” of the digital age it should be nationalised and the algorithm should be removed.
Now I’m looking at my iPad and iPhone and wishing I could manage them through Nix too.
I’d put it at a comparable difficulty to learn / powerful tool as git. Which given that they’re both based on hash trees makes sense.
I had a hard time grasping why the Axiom of Choice / Law of the Excluded Middle was so problematic until I heard it translated into a Computer Science context.
The Law of The Excluded Middle sounds very reasonable at first. For all propositions P, P ∨ ¬P. i.e. Every proposition is either true or false. Sounds fine right? But when viewed in the context of computer science via the Curry-Howard Isomorphism. A proposition is actually a program, and deciding the truth value of a proposition involves "running" that program. So The Law of the Excluded Middle is actually the Halting Problem! It's really saying that all possible programs terminate and yield true or false, but we know that some programs don't terminate, some propositions aren't true or false, but undecidable.
So circling back around to the Banach-Tarski paradox. I would be very skeptical of any paradoxes resulting from assuming the halting problem doesn't exist!
The burden of using these extreme approaches is high, but there are definitely circumstances where it is warranted. Think of it as TDD on steroids.
Go espouses "Share by communicating, don't communicate by sharing" i.e. don't let goroutines communicate by mutating shared data, but then doesn't provide any effective immutable data structures to make this easy.
Being able to safely send pointers to immutable maps over channels would make go very nice to work with. Although I'll never use Go outside of work until they remove nullable pointers which seems unlikely.
The paper uses the Casimir effect to avoid the need for negative mass.
However I do wonder if it’ll turn out that these higher dimensional geometric problems turn out to have the same structure as Godel’s proof. That the higher dimensional geometric structure is complex enough to represent their own foundation.
Although now I’m committing the same fallacy I was arguing against i.e. an equivalence between unknowns
It’s not this mystical thing that people make it out to be online.