jojo3000

Sorry, I was unclear. I meant that most LCF style theorem provers only have one theorem datatype to carry proof information.

Tensors are a good example: In a proof you might want to do induction over the dimensions of a tensor. This means your type of tensors needs to contain all tensors of all dimensions. But working on the type of all tensors is not so nice anymore: a lot of algebraic properties do not hold, they only hold for tensors of a specific dimension. An example is the Tensor library in the Deep_Learning AFP entry.

Now in Isabelle most strutures are encoded as type class, but when your type is not anymore in the type class suddenly you need to proof a lot of theorems yourself, and the automation does not work as nice as with type classes. Generally, in HOL provers you want at least that your type at least has nice algebraic properties on the entire type. If this is not the case proofs get much more convoluted. Isabelle's simplifier supports this case using conditional rewrite rules, but it still does not work as nice as using type inference to handle this cases.

In dependent type theorem provers it isn't a problem to proof everything on tensors with a fixed dimension. When a proof requires to do induction on the dimension itself these kind of shape can always constructed in the proof itsefl.

The memory consumption will surely be better, as HOL or Isabelle will only store the fact that a theorem was proven, but not how. But then Lean can store the proofs and has two independent external type checkers. Isabelle has the infrastructure to do this, but it can not cope with it after a certain size (Isabelle's HOL-Proof does not even contain all of HOL/Complex_Main). In my experience Lean feels much faster than Isabelle, so I would guess the proof will take much longer than in Lean. But I don't have any concrete measures.

In Isabelle one might want to trust the code generator to evaluate certain computations in ML.

But your "intermediate specifications" are not part of your specification! The specification says that the result is a sorted version of the input. It does not care about the induction hypothesis in your program. It might be technically necessary depending on the verification condition generator you are using. When you verify a functional program using Isabelle, Lean, or Coq your statement is that the output is a sorted version of the input.

Lean is LCF style in the sense that there is a small kernel, and all proofs written by the user and generated by the automation are checked by this kernel. This kernel (i.e. type checker) is much smaller than that of Coq or Agda.

It is _not_ LCF style in the sense that there is only a "theorem" datatype with proof operations. Lean proofs are type-checked expressions.

It is hard to find a terse description of the Calculus of Constructions or CIC. Lean's logic essentially consists of Martin-Löf type theory + (noncumulative) universes with Impredicative Prop + inductive type (where nested and mutual induction is compiled down to a simpler forms with only one eliminator) + quotient types + function and Prop extensionality. And optionally choice to gain a classical logic. Most other features, like a Agda like dependent pattern matching, or mutual and nested inductive types are compiled down to more basic features.

This is orthogonal. But first, there are still buffer overflows, null pointer accesses & segmentation faults, etc. in the kernel happening. And this is a big problem!

But lets assume this is solved. Then a API can be checked for certain properties. You can specify what it means that something is read-only in an environment etc. And ensure that it is enforced by the operating system.

As example: the verification of seL4 not only guarantees avoidance of classical security holes (buffer overflows etc.) but also certain non-interference properties.

There was also a presentation on Bus1 on the systemd.conf 2016: https://www.youtube.com/watch?v=6zN0b6BfgLY

If behind the USB port is some (writeable) data storage (for PDF manuals etc) this is quite possible.

Which is very unfortunately. It would be nice to have Hurd running on seL4!

Even defining the real numbers is already quite involved, for example in Isabelle/HOL it is introduced as quotient over Cauchy sequences:

http://isabelle.in.tum.de/dist/library/HOL/HOL/Real.html

This is the classical way (and similar to HOL Light or HOL4). AFAIK in Coq the standard way is to introduce the reals axiomatically.

The bottom theories in http://isabelle.in.tum.de/dist/library/HOL/HOL/ are all about classical real analysis, based on topology and real-normed vector spaces.

In interactive theorem proving HOL4 (http://hol.sourceforge.net/) and Isabelle (http://isabelle.in.tum.de/) are written in SML and are actively developed.

Some of his arguments look a little bit botched.

For example: > Fallacy #1: "Systemd is multiple binaries, therefore it is not monolithic"

Well following Wikipedia (http://en.wikipedia.org/wiki/Monolithic_application) means either a non-modular application, or a self-contained application. In this sense either his counter-argument is simply wrong, or the examples list he gives at the and is wrong.

> Fallacy #4.1: "Unit files reduce complexity"

Here he compares the ca. 275.000 LoC of systemd with the 10.000 LoC of shell scripts used as initscripts on Debian. Lets ignore that the 275.000 LoC contains much more than the unit management in the systemd daemon. But why are the bugs always in the scripts and never in the shell as he claims? And sorry, I don't take his word that C is always more error prone than the shell. This is true when the shell is used for its intended purpose: to start commands, pipe btw them and having a little bit of flow control. For everything else you surely want to have a general purpose language.

> Fallacy #7: "Systemd gives you socket activation!"

Well, according to boot charts, socket activation is not only a marketing gimmick.

EDIT: Add Fallacy 7