You are clearly misinformed. According to German law, you can start a UG (limited) with only 1€ + notary cost. Starting a business with personal liability doesn't cost anything.
It's beyond me why anyone would downvote that. An UG is uninvestable, and a GmbH would also scare most investors. Anything but an AG is not going to work.
What are you talking about..? A GmbH is the German equivalent of an Ltd. An AG is a publicly traded company and thus not something investors are looking for. Also, the majority of companies in Germany are just ordinary eigetragene Kaufmänner (so normal businesspeople like your average plumber), or GmbH (literally any other company that isn’t a stock market traded enterprise).
We're talking about VC investing here, not your local currywurst kiosk.
> An AG is a publicly traded company
Falsch. An Aktiengesellschaft is a corporate form that protects the investors and mandates a certain formal governance and management structure. It has nothing to do with being publicly traded.
For the same reasons, VCs will be very wary of investing in a Delaware S Corp (similar to a GmbH) instead of the preferred C corp (similar to an AG), even if the company is fully private and has no revenue.
> Also, the majority of companies in Germany are just ordinary eigetragene Kaufmänner (so normal businesspeople like your average plumber), or GmbH (literally any other company that isn’t a stock market traded enterprise).
> It has nothing to do with being publicly traded.
It is, in most cases. Tell me about a startup that started off as an Aktiengesellschaft as opposed to a GmbH? Why would you even want to put 50k in instead of 25k, deal with all the governance overhead and reporting duties? It makes no sense at all, and during all the VC conversations I had, never once was a GmbH mentioned as problematic.
> Irrelevant.
It's not to the claim that you cannot found a company in Germany without putting down a significant amount of money and a notary. You just moved the goalposts.
AG is required for going public, however it's not a legal requirement that only public companies do so. You're mistaking cause and effect.
> Tell me about a startup that started off as an Aktiengesellschaft as opposed to a GmbH? Why would you even want to put 50k in instead of 25k, deal with all the governance overhead and reporting duties?
This is one of the big problems with German companies, and the reason why even German founders will start directly as a Delaware company instead. The capital requirements are $100 and reporting very minimal.
> It's not to the claim that you cannot found a company in Germany without putting down a significant amount of money and a notary.
I claimed that a non-AG makes it uninvestable, not what you're saying here (which is the product of your imagination). A GbmH has strict requirements that adding a new owner (an investor) must be done in front of a notary, and if your angel investors are all over Europe or the world, you'll have to tell them that they either they have to fly to Germany or find a German lawyer and give the lawyer a PoA. That's way too much hassle for most people, and the result is you'll hear a polite "no thanks, I might reconsider if you move your company to US/UK/Singapore". At least investing in an AG can be done without notarization.
A non-AG in Germany will inherently chase away almost all international investors. If you're lucky enough to find an international investor that's really interested, the most likely thing you'll be told is to either switch to AG or, preferably, re-incorporate in US/UK/Singapore and only then will your company be investable.
> You just moved the goalposts.
No, that's your misunderstanding. I mentioned a non-AG being unviable for international investors because they're the only ones worth mentioning. Local ones in Germany are mostly irrelevant for various reasons: they're either too ignorant of a specific market segment, too stingy, want too much control, only invest in later stages but not pre-seed, etc... You have to be really desperate to look for German investors, and that's true in most EU countries. The good VCs tend to be based in UK, Sweden or Estonia, with few exceptions. Angels are everywhere, but mostly outside Germany and they just won't bother with notarization for 20k EUR.
No. The whole point of the LCF approach is that only kernel functions can generate theorems. Usually this is done by having a Thm module with opaque thm type (so its instances can only be generated by this module) and embedding the base rules of your logical calculus as shallow functions into that Thm module. Thus, all thm objects are correct by construction (w.r.t. your calculus), and you only need to check the Thm module to verify this.
Tactics generate thms by calling functions of the Thm module in some fashion.
At least in Isabelle/ML, it seems like in practice there are also untrusted "oracles" that a proof can invoke to generate "thm" objects [0], and it's not entirely trivial to automatically ensure that only trusted sources are used in a project [1], unless I am misunderstanding the linked thread.
Of course there's no free lunch, as you say, in making sure that high-level proofs are lowered into the trusted part correctly, but it's certainly a piece that should ideally be as simple as possible.
This does not resolve the issue of how to ensure that the "module" system is itself sound and has no unforeseen escape hatches. You have to assume that it is, or else include a complete programming language implementation as part of your TCB. If your system generates proof objects (possibly allowing for some kind of reflection, with the proof objects merely specifying some kind of computation) you can skip this and simply prove that the kernel itself is correct.
The question: "does the ambient programming language do the right thing?" applies to other provers too. So if you assume the semantics of the implementation language is broken, or the compiler, or the computer executing the code, then those issues also need to be added to the TBC of Curry-Howard provers.
In the described case, this was a simple user error. But you are right nonetheless: To enable the concurrency, the system uses a parallel inference kernel (https://www21.in.tum.de/~wenzelm/papers/parallel-isabelle.pd...). I have heard the anecdote that in the first version, this also allowed one to prove false, by fulfilling a proof promise with a proof that depended recursively on the same promise.
And there are verification tools for verification tools! Isabelle has a verified proof checker that can check whether a given proof is sound: https://www21.in.tum.de/~rosskops/papers/metalogic_pre.pdf
The only caveat is that the proof checker itself is verified in Isabelle...
Indeed this can simply be checked by a command-line invocation.
But I don't think the student was aware: They would only have seen a purple coloring of the "stuck" part, as shown in the linked example in the blog post. And if one assumes that the system only accepts correct proof steps, it's very easy to miss a small error in a theorem statement...
