jojo3000

4 ms·

1.
SpaceX Buys over 1000 Cybertrucks(finance.yahoo.com)
2 points by jojo3000 9mo ago|1 comments
2.
by jojo3000 9y ago
Sorry, I was unclear. I meant that most LCF style theorem provers only have one theorem datatype to carry proof information.
3.
by jojo3000 9y ago
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 any
4.
by jojo3000 9y ago
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 infrastruc
5.
by jojo3000 9y ago
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 techn
6.
by jojo3000 9y ago
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
7.
by jojo3000 10y ago
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
8.
by jojo3000 10y ago
There was also a presentation on Bus1 on the systemd.conf 2016: https://www.youtube.com/watch?v=6zN0b6BfgLY
9.
by jojo3000 10y ago
If behind the USB port is some (writeable) data storage (for PDF manuals etc) this is quite possible.
10.
by jojo3000 11y ago
Which is very unfortunately. It would be nice to have Hurd running on seL4!
11.
by jojo3000 11y ago
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 Thi
12.
by jojo3000 12y ago
In interactive theorem proving HOL4 ( http://hol.sourceforge.net/ ) and Isabelle ( http://isabelle.in.tum.de/ ) are written in SML and are actively developed.
13.
by jojo3000 12y ago
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_