Well, Lean is written in Lean, so I am pretty sure a runtime bug like this could be exploited to prove `False`. Yes, since the kernel is written in C++, technically it's not the part affected by this bug, but since you cannot use the Lean kernel without the Lean compiler, this difference does not matter.

  def clamp (value min max : Float) {H : min < max} : Float := ...

what

99% of the time their reasoning is laughable. Or even if their reasoning is on the right track, they often just ignore it in the final answer, and do the stupid thing anyway.

I think you could basically copy your comment into an FAQ section or something on the front page.

I think you could prove that you can't construct a sound & complete type system for Lua. But just saying "Your type system cannot be sound" by itself is definitely wrong. I don't understand why people are throwing out both soundness & completeness, instead of at least retaining one (and I think the choice here is pretty obvious, a sound but incomplete type system is much more useful than an unsound one).

From Flow's website[1] (a type checker for JavaScript):

> Flow tries to be as sound and complete as possible. But because JavaScript was not designed around a type system, Flow sometimes has to make a tradeoff. When this happens Flow tends to favor soundness over completeness, ensuring that code doesn't have any bugs.

I don't understand why other type systems for dynamically typed languages cannot strive for that, and in particular I am pretty salty at TypeScript for explicitly not caring about soundness.

[1]: https://flow.org/en/docs/lang/types-and-expressions/#toc-sou...

Also, are there any Lua constructs that are difficult/impossible to type?

Is type checking decidable? (Is the type system Turing complete?)

(I don't get the value of your AST checksumming idea over just checksumming the source text, which is what almost all distro packages do. I think the number of changes that change the code but not the AST are negligible. If the code (and AST) is changed, you have to audit the diff no matter what.)

The more interesting question that does not have a single good answer is how to do the auditing. In almost all cases right now the only metric you have is "how much you trust upstream", in very few cases is actually reading through all the code and changes viable. I like to look at how upstream does their auditing of changes, e.g. how they do code review and how clean is their VCS history (so that _if_ you discover something fishy in the code, there is a clean audit trail of where that piece of code came from).

When I personally package stuff using Nix, I go out of my way to build everything from source as much as possible. E.g. if some repo contains checked in generated files, I prefer to delete and regenerate them. It's nice that Nix makes adding extra build steps like this easy. I think most of the time the motivation for having generated files in repos (or release tarballs) is the limitations of various build systems.

Comments URL: https://news.ycombinator.com/item?id=41117855

Points: 2

# Comments: 0

Looking forward to sharing this with colleagues. On one hand I am excited because I think this bottom-up approach is the correct way of understanding git, on the other hand I am afraid that they will think it's difficult to understand and just not bother. (Again I can't fathom how programmers, who you know, learned programming, which is quite a steep learning curve in itself for first time, shy away from learning git properly, a tool that's just as important to their daily work as whatever programming language they are using.)

Comments URL: https://news.ycombinator.com/item?id=38255561

Points: 2

# Comments: 0

Comments URL: https://news.ycombinator.com/item?id=36490811

Points: 2

# Comments: 0