Proofcheckers can be used to verify the correctness of proofs, which - in turn - can prove the correctness of programs. In theory. In practice, there is a slight problem: All of the modern proofcheckers are implemented in some high-level functional language, and their runtimes tend to be rather complicated. And they are not verified themselves.

There is the common concept of the "trusted codebase": You have to start with something, and the trusted codebase is the amount of program code you have to trust. Unfortunately, trying to keep the trusted codebase small while keeping proofs simple are contrary goals.

Coq addresses this problem by having a small kernel that checks the proofs, and lots of unverified code that produces proofs. This way, proving even complicated theorems becomes bearable. However, this can also result in regressions with newer versions of Coq: Tactics might do things differently in different versions, and automatic variable names might change. The common solution is to try to write proofs that do not depend on those names, or at least explicitly give these names. It is, however, not always possible. In theory, it is possible to export the proofs into a common format which is (mostly) version independent, but doing that is like saving compiled libraries to prevent compiler incompatibilities: Specifications tend to change, and proofs should therefore be maintainable, and maintainable proofs can always be ported to newer versions of Coq.

The situation is not perfect, but at least, no false proofs are accepted - mostly. There have been bugs that allow deriving False, and therefore everything else. This is a common criticism of program verification - how trustworthy can an unsound proofchecker be? But think about what we are actually talking about: People have written an algorithm, have thought about an informal proof ("proof in words") that would otherwise be accepted, and then formalized it for a proofchecker that has a bug which is usually some exploit of an edge case. I think a scenario where this actually leads to a bug in the resulting program code is highly unlikely. I wonder if something like that ever even occured. I think, in conclusion one can say, a verified implementation is usually formally correct, and it is almost impossible for it to not satisfy the specification. And, above all, you do not lose anything: You will have to write code anyway, the process of verifying it will not introduce additional bugs.

That being said, it is – of course – very desirable to have a correct proofchecker. Ideally, it should be metacircular. To make it less prone to bugs, it is desirable to keep it as simple as possible. I tried to implement a simple proofchecker several times, but I always failed because at some point I didn't find it sufficiently simple anymore. In a functional language with algebraic types and automatic garbage collection, it might not be too hard — but also not elementary. OCaml, Standard ML and Haskell have sophisticated runtimes which might be a good thing when writing unverified high-level code, but for my taste, it is rather complicated for a proof checker. So I was thinking about what is needed to write a realistic proof checker.

I think, in the current situation, it is unrealistic to go to a lower abstraction level than C: C is the lingua franca. However, it is probably a good idea not to use C as a "portable assembler", but rather have a clean and obvious programming style rather than focussing on efficiency.

One reasonable way of encoding the several recursive definitions is using structs, unions and enums. It is probably the easiest way, but probably not the most efficient representation, but it should be portable and the resulting code should be readable. However, this results in complicated memory management. Any implementation would probably have lots of allocations of small structs that point to each other. Allocating objects can be done with malloc(3), but usually, malloc(3) is not meant to manage many small objects. A slice allocator on top of malloc(3) would solve that problem. But then again, malloc(3) bases on mmap(2). It would also make the implementation more complex.

Allocating and deallocating objects can be done directly in the code, but as this is done frequently, it is probably not a good idea to always do this explicitly. A copying garbage collector would probably be the best for this situation, and a simple copying garbage collector is probably bearable – however, it would increase the trusted codebase. Using a reference counter would also be sufficient, and one could simplify it a lot using __attribute__((__cleanup__())) from GCC. Still, all of those possibilities – including manual memory management – are rather complicated

The question is whether deallocating objects at all is necessary. As The Old New Thing points out, the null garbage collector is correct. A proof checker gets axioms and already proved theorems, a conclusion and a proof as input, and its only objective is to check whether this proof is correct, and maybe return an error message that indicates the error. A simple stack-oriented language that is sent through stdio should be sufficient, and therefore, it might be sufficient to never actually deallocate. This would be the UNIX way, probably: Do one thing and do it right. If it occurs that not enough memory is available for some proof, one could preload libgc.

At some point, the question is whether all of this is worthwile at all. One could just use C++ and std::shared_ptr and be happy. But then, the additional complexity of the C++ runtime arises. Well, LEAN appears to be written in C++, but I don't know about its memory management.

To this point, it is questionable whether it is really worthwile to try to write a typechecker only using low-level programming techniques, rather than relying on well-tested abstractions. Besides the already mentioned small likelihood of a critical bug in typecheckers that leads to wrong proofs of algorithms, even in the presence of such a bug, it would only have to be fixed once, so after 30 years without critical bugs, one could be pretty sure that everything works fine.

Of course, this is not the only reason for wanting an implementation of a proof checker in C. All the Systems appear to try to create an own programming language. I would rather like to have a library which I can use in the language of my choice. On the other hand, Coq has a way of calling external programs to provide proofs, which is in many cases equivalent to such a library.

External Content not shown. Further Information.

Popular Culture:

• Schluss mit Wildtieren im Zirkus!
• Milliardenverluste durch Werbeblocker ~ Leute! Werbung wird nicht "geblockt"! "Blocken" klingt so aktiv. Sie wird lediglich nicht abgerufen und dargestellt.

Science, Software, Hardware:

• 6 Reasons You Can't Trust Science Anymore
• On Sufficiently Smart Compilers

Comics/Images/Audios/Videos:

• cenobite for president
• Free Slaves
• Black People
• If we label GMO's
• Signal
• Jihad's

External Content not shown. Further Information.

Popular Culture:

• Cocktails atmen statt trinken
• Nuremberg produces record 460m pencil
• Häftlinge sind offline ~ tolle Parallelgesellschaft, die wir uns da in den Gefängnissen züchten; what could possibly go wrong?

Nerd Culture:

• IT Department Creates Giant Hamster Wheel Out Of 36 iMac Boxes

Science, Software, Hardware:

• Banken wollen Facebook-Freunde als Entscheidungsgrundlage für Kredite nutzen ~ oh nein, Facebook benutzt unsere Daten um Geld zu verdienen. Das konnte ja keiner ahnen! Und es ist auch völlig absurd mit Besorgnis zur Kenntnis zu nehmen, dass die erste Krankenkasse für eine Apple Watch zahlt
• hemispherical omnidirectional gimbaled wheel
• AI-Powered App for Legal Help
• Infinitary Species

Zeroth World:

• Bilder in Kaffeetassen auf Milchschaum drucken
• Giant Minion Causes Havoc in Ireland

Comics/Images/Audios/Videos:

• Langer Anlauf

Quotes:

• What's the difference between a taliban outpost and a pakistani elementary school? Don't ask me, I just fly the drones.

External Content not shown. Further Information.

Again no comic. Sorry.

Popular Culture:

• Denmark Bans Kosher and Halal Animal Slaughter ~ “Animal rights come before religion,” Danish minister for agriculture and food Dan Jørgensen told Denmark’s TV2 ~ In my humble opinion, this is the wrong question: Nobody forces jews and muslims to eat meat at all. It is rather banning a specialized form of gourmet food because it is harmful to animals, like the German ban of foie gras.
• Tropische Hölzer in Holzkohle ~ wtf?

Science, Software, Hardware:

• Writing Hello World Bootloader
• Portable, Inflatable Bathtub
• The Two-Foot-Wide Sea Star

Comics/Images/Audios/Videos:

• Volker Pispers über den IFO Geschäftsklimaindex ~ und auch der Rest ist genial.
• Name
• 7 Deadly Sins
• Quality Time
• Ketchup
• Drug Use

External Content not shown. Further Information.

Die Deutschen™ wollen mehr Mitspracherecht der Bürger in der Wissenschaft.

Und wer sollte die Forschungs-Milliarden für diese Projekte verteilen? Das sollten „die Bürger“ entscheiden, ist mit 42 Prozent die häufigste Antwort.

Die selben Bürger, die dafür gesorgt haben, dass man in Deutschland kein Humaninsulin herstellen durfte? Die selben Bürger, die demokratisch einen Atomausstieg, einen Atomausstiegausstieg und einen Atomausstiegausstiegausstieg innerhalb von 20 Jahren gewählt haben? Die selben Bürger, die ihre Kinder zu Masernparties mitnehmen, und angst vor Strichcodes haben?

Die wollen jetzt darüber entscheiden, wie man am besten Geld für Wissenschaft investiert?

External Content not shown. Further Information.

Sorry. Too much work. No comic this week.

Popular Culture:

• Fordern Sie Obi auf, den Verkauf von Tieren zu beenden! ~ ich wusste garnicht dass das überhaupt noch erlaubt ist.

Nerd Culture:

• Fiske Reading Machine

Science, Software, Hardware:

• Winziger Adapter mit magnetischem Ladekabel für Smartphones
• Rowhammer, jetzt auch mit JavaScript ~ nachdem bei mir nicht mal der native exploit funktioniert, sehe ich das jetzt mal gelassen.
• What happens when you put a coin into a block of dry ice
• Hair ice
• Gesendete E-Mails lassen sich mit Dmail wieder zurückholen ~ von der Idee her konvergiert das wohl gegen Internet Mail 2000.
• Websites, Please Stop Blocking Password Managers ~ agreed.

Zeroth World:

• Warum Kühe magnetisch sind ~ sollte das nicht eigentlich unter das Apple-Patent auf MagSafe-Stecker fallen? Immerhin ist der Magen der Kuh ja sowas wie ein power supply.
• Tierschützer rüsten Nashörner mit Alarmsytem aus ~ das ist eine gute Idee, dann können deutsche Autofahrer einfach darauf umsatteln, Nashörner zu reiten. Das wird die Population wieder aufstocken.

Comics/Images/Audios/Videos:

• sole food
• evolution
• cash craft ~ same idea as one of my former comics
• if at first you don't succeed
• peer pressure
• pick up lines
• priorities

Quotes:

• Diet Tipyour pants won't get too tight if you don't wear any

External Content not shown. Further Information.

The day I began writing this post was one of those rare days when I watched TV. Passively of course. It was about worried parents, and experts™ who fear that smartphones might be dangerous for children. I remembered that in bavarian schools, smartphones are forbidden. When I was a young child, people were worried that cartoon violence could make children violent. Then they were worried that video games were addictive and would harm children. Then computers and instant messaging. Well, we all exist. And most of us only suffer moderately.

It might be that some children actually had problems due to trends and technology. It might even be severe damage. Progress takes its toll. But on the whole, progress has improved and saved life, and it will probably continue. Probably we should, instead of blocking progress, try to be less of an asshole society, and actually help and support the people who had bad luck.

Some people might think that the use of modern technology is a way youth wants to set itself apart. But remembering my childhood, children rarely tried to keep it a secret: We always wanted to talk to grown-ups about the games we played, about the cartoons we saw, &c – they were just not interested. Maybe it would be the best for the children to actually care about what they do – even though it may not be interesting by itself. And by caring I mean really trying to understand it, not only half-heartedly worrying how it could possibly harm them. It is the world in which your children live, and that alone should make it interesting as a parent. If you are not willing to do that, do yourself and your would-be children a favor and just do not become a parent.

External Content not shown. Further Information.

Popular Culture:

• Spam-Rate erstmals wieder unter 50 Prozent ~ dafür ist die Erfolgsrate beim Mailempfang aber inzwischen auch recht niedrig.
• Zoll zerstört Mainboard wegen pistolenförmigem Kühler
• Die einzige Partei, die Flüchtlings-Wahlkreise forderte

Nerd Culture:

• Transparent Practice Padlock For Budding Locksmiths
• How Sci-Fi Ships Stack Up
• Fliegendes Spaghettimonster vs. GEZ ~ überrascht mich nicht.

Science, Software, Hardware:

• Wissenschaftlerin sagt "kleine Eiszeit" für 2030 voraus
• Löchrige VMs: Den PGP-Schlüssel des Nachbarn klauen

Zeroth World:

• NSFW Sexpuppen werden mit künstlicher Intelligenz ausgestattet

Comics/Images/Audios/Videos:

• Existence is futile
• Wheelchair
• Undone
• Did you hear that?
• Pluto
• Art
• Invention
• Dinner Friends
• Paranormal Activity: Digital Visitors
• Andrea Berg: Die Hitkollektion ~ du hast mich 678 mal belogen.
• David and Goliath
• Finger Evolution
• Rice
• Caterpillar

Quotes:

• „wir können unmöglich erlauben, dass eine Wahl etwas verändert“ (Wolfgang Schäuble)