The version I heard involves a 3d artist adding an obnoxious fairy flying around the character, so not critical, but noticable.
I also think the idea here is to apply it to bosses who's self-worth seems to be tied to putting their mark on the product without being burdened by knowledge. (Because they'll want to change something regardless of the state)
I recommend the natural number game (also mentioned above) for a casual introduction to the mathematics side, just to get a feeling.
If you are serious about learning lean, I recommend Functional Programming in Lean for learning it as a programming language and Theorem Proving in Lean for learning it as a proof assistant
I think the difference is mostly cultural. The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.
Many people in the Rocq community see this as a no-go and some argue this will cause the system to be hard to use over the long run. In the Lean community, the interest in type theory is at a much lower level, and people see this as a practical tradeoff. They recognize the theoretical issues show up in practice, but so infrequently that having this axiom is worth it.
I consider this matter to be an open question.
If you look at what's being done in the communities, in Lean the focus is very much on and around mathlib. This means there's a fairly monolithic culture of mathematicians interested in formalizing, supplemented with some people interested in formal verification of software.
The Rocq community seems much more diverse in the sense that formalization effort is split over many projects, with different axioms assumed and different philosophies. This also holds for tooling and language features. It seems like any problem has at least two solutions lying around.
My personal take is that this diversity is nice for exploring options, it also causes the Rocq community to move slower due to technical debt of switching between solutions.
> The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.
Couldn't you introduce proof relevance as an explicit axiom into a Lean program to solve that particular issue?
In a lot of cases you can get far by locally proofreading the definitions.
Trying to formally prove something and then failing is a common way people find out they forgot to add an hypothesis.
Another pitfall is defining some object, but messing up the definitions, such that there's actually no object of that kind. This is addressed by using test objects. So suppose you define what a ring is, then you also prove that real numbers and polynomials are examples of the thing you defined.
I'd also like to know more about that. My comment points out some things about HoTT that might be described as "downsides" by some but are more like things that people might expect from HoTT given that it 'handles' type equality in a rigorous yet flexible way, but aren't actually feasible in a rigorous treatment, i.e. the system is not going to pick up all the issues that are "brushed aside" in an informal treatment and resolve them on its own. Its behavior will point out to you that these issues exist, but you'll still have to do a lot of work dotting the i's and crossing the t's, as with any formalization.
I joined binwiederhier for a while in developing Syncany and he invited me for an internship at his current employer.
The experience I gained both in contributing to Syncany and said internship helped me indirectly land the role I'm currently in, and my open source experience in general helped me land a cool engagement where I got to do some innovative open source projects.
Oh man, Pim! What a small world. I looooved working with you on Syncany, and I tried so hard to recruit you hehe. I looked you up on LinkedIn the other day and it looks like you're doing amazingly.
Ping me and we'll chat if you like. I'm working on a new open source project [1] that needs your help, hehe.
I saw CT and I was like "hmm I wonder where in CT" and then I noticed the username. I kinda sorta know you IRL, so definitely a small world :D (worked at the same CT company)
First time I recognized someone on HN so I have an uncontrollable urge to tell someone.
Pushover is fantastic, and if you are happy with it, then stick with it :-) I've never used Pushover, so I don't actually know all that well.
However, ntfy is 100% open source so you can self-host it if you like, and I believe it does have a bunch of features that Pushover does not (email notifications, email publishing, scheduled delivery, tags/emojis, phone calls, icons, ... see for yourself: https://docs.ntfy.sh/publish/). I'm sure ntfy is missing things too that Pushover has. I'll let you be the judge of it.
And yes, it's a reference to the song. Good catch. I was listening to it 20 years ago or something like that when I had to come up with a new username. And it stuck. ;-)
Not strictly what you're looking for, but in Lean (functional language/theorem prover), there's some interesting work being done. Using the tool actually shows which suggestions will compile, which certifies correctness to some degree. https://leandojo.org/
I also think the idea here is to apply it to bosses who's self-worth seems to be tied to putting their mark on the product without being burdened by knowledge. (Because they'll want to change something regardless of the state)
reply