hannes/hannes.robur.coop
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

typos

Browse source
This commit is contained in:
Hannes Mehnert 2016-04-10 09:12:39 +01:00
parent 7bd050d6d6
commit a94d5375bc
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Posts/About
View file

@ -15,7 +15,7 @@ While I know how to solder, I don't plan to write about hardware in here. I'll
assume that off-the-shelf hardware (arm/amd64) is available and trustworthy. assume that off-the-shelf hardware (arm/amd64) is available and trustworthy.
Read the [Intel x86 considered Read the [Intel x86 considered
harmful](http://blog.invisiblethings.org/papers/2015/x86_harmful.pdf) paper in harmful](http://blog.invisiblethings.org/papers/2015/x86_harmful.pdf) paper in
case you're interested in trustworthyness of hardware. case you're interested in trustworthiness of hardware.
My current obsession is to enable people to take back control over their data: My current obsession is to enable people to take back control over their data:
simple to setup, secure, decentralised infrastructure. We're not there yet, simple to setup, secure, decentralised infrastructure. We're not there yet,
@ -79,9 +79,9 @@ I concluded two things: formal verification is hard and usually not applicable
for off-the-shelf software. *Since we have to rewrite the software anyways, why for off-the-shelf software. *Since we have to rewrite the software anyways, why
not do it in a declarative way?* not do it in a declarative way?*
Some artifacts from that time are still around: an [eclipse plugin for Some artefacts from that time are still around: an [eclipse plugin for
Coq](https://coqoon.github.io/), I also started (with David) the [idris-mode for Coq](https://coqoon.github.io/), I also started (with David) the [idris-mode for
emacs](https://github.com/idris-hackers/idris-mode). Idris is a depedently emacs](https://github.com/idris-hackers/idris-mode). Idris is a dependently
typed programming language (you can express richer types), actively being typed programming language (you can express richer types), actively being
researched (I would not consider it production ready yet, needs more work on a researched (I would not consider it production ready yet, needs more work on a
faster runtime, and libraries). faster runtime, and libraries).

6
Posts/OperatingSystem
View file

@ -60,13 +60,13 @@ is then done by resource usage (time, bandwidth, storage).
Ok, now we have hypervisors which already deals with memory and scheduling. Why Ok, now we have hypervisors which already deals with memory and scheduling. Why
should we have the very same functionality again in the virtual machine? should we have the very same functionality again in the virtual machine?
Additionally, earlier in my live (back in 2005 at the Dutch hacker camp "What Additionally, earlier in my life (back in 2005 at the Dutch hacker camp "What
the hack") I proposed (together with Andreas Bogk) to [phase out UNIX before the hack") I proposed (together with Andreas Bogk) to [phase out UNIX before
2038-01-19](https://berlin.ccc.de/~hannes/wth.pdf) (this is when `time_t` 2038-01-19](https://berlin.ccc.de/~hannes/wth.pdf) (this is when `time_t`
overflows, unless promoted to 64 bit), and replace it with Dylan. A [random overflows, unless promoted to 64 bit), and replace it with Dylan. A [random
comment](http://www.citizen428.net/blog/2005/08/03/what-the-hack-recap/) about comment](http://www.citizen428.net/blog/2005/08/03/what-the-hack-recap/) about
our talk on the Internet is "the proposal that rewritting an entire OS in a our talk on the Internet is "the proposal that rewriting an entire OS in a
language with obscure sytanx was somewhat original. However, I now somewhat feel language with obscure syntax was somewhat original. However, I now somewhat feel
a strange urge to spend some time on Dylan, which is really weird..." a strange urge to spend some time on Dylan, which is really weird..."
Being without funding back then, we didn't get far (hugest success was a Being without funding back then, we didn't get far (hugest success was a