Viewing profile — 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 dimension…

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 ind…

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 induc…

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 c…

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 assu…

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…

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.wiki…