jroesch

16 ms·

31.
by jroesch 10y ago
We have plans to implement a framework for writing high performance, GC free programs in Lean ( http://leanprover.github.io/ ). We have spent the last year addressing shortcomings of the previous version and will be shipping
32.
by jroesch 10y ago
There have already been two file system verification projects, this year's OSDI best paper is the most recent example, http://locore.cs.washington.edu/papers/sigurbjarnarson-yggdr... , and last year as SOSP FSCQ:
33.
by jroesch 10y ago
Yeah I think SMT is really the state-of-the-art right now in this area. Leo De Moura (one of the main authors of Z3) has been working on Lean for the past couple of years. There is a small group of us (5~) who have been working on a big rel
34.
by jroesch 10y ago
A short answer is that the theory is just simpler. Non-dependent type theory spends a lot of effort separating values, types, kinds and valid operations over them. For example you need lots of extensions to make it possible to use a type bo
35.
by jroesch 10y ago
The core theory (and implementation) is much simpler for almost all dependent type theories. At least this is my personal feeling after having read a lot of GHC code, written an Idris backend, the native backend for Lean, and significant po
36.
by jroesch 10y ago
Type inference isn't the most important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible. Not to mention you can get pretty good "inference" in dependentl
37.
by jroesch 10y ago
You don't need type theory to verify program properties, people have been using first-order methods for decades to prove properties about programs. For example there was a line of work in ACL2 that verified a microprocessor implementat
38.
by jroesch 10y ago
The problem with an optimization like this is that the current approach always gives you a guarantee on runtime cost. Heuristic based optimizations make performance harder to ensure, not to mention recovering performance when you fall out
39.
by jroesch 10y ago
I feel like you have confused quite a few concepts here. First, type theory based proof assistants (like Coq) and model checkers are very different tools with very different guarantees. Most model checkers are used for proving properties ab
40.
by jroesch 10y ago
At least in programming languages, systems, and formal verification project code is both available and often evaluated along side the publication. For example FSCQ( https://github.com/mit-pdos/fscq-impl ) from MIT, Verdi
41.
by jroesch 10y ago
I think they made a much better decision then everyone else even if verbose. Nearly every language has continued to repeat Tony Hoare's "billion dollar" mistake of allowing null to inhabit any type. I think approaches like Ru
42.
by jroesch 10y ago
If you are willing to adopt a strong enough type system pretty much any interesting property about a program you want to prove is provable. Its just a matter of ergonomics, more complex type systems provide power, but require investment in
43.
by jroesch 11y ago
A comment/correction `io` is stable, its just `chars` directly on a type that implements `Read` that is still unstable, the majority of `std::io` is stable these days.
44.
by jroesch 11y ago
Its actually much easier then it sounds, we had an undergrad write an entire windowing system on-top of implementing the rest of the OS for undergraduate operating systems at UW in a single quarter (2.5 months~).
45.
by jroesch 11y ago
I think you guys might find Arrakis interesting: https://arrakis.cs.washington.edu/ it won Best Paper at OSDI '14 and demonstrates a possible way to better use things like virtio.
46.
by jroesch 11y ago
I think the pain only appears when you start trying to do "deep specification" of large systems. My research group has about 5-10 of us that have all built large systems (5-60 kloc) and verified them in Coq. I know each of us long
47.
by jroesch 11y ago
You are correct the current proposed C++ coroutines are vastly different then M:N userspace threading. The allocation differences are drastic, and unlike Go they play nicely with system libraries.
48.
by jroesch 11y ago
Do you have a compelling use case? I can't imagine a use for untagged unions in Rust that isn't subsumed by other features in the language.
49.
by jroesch 11y ago
Steve has hit this on the head, there are lots of places where we are using older abstractions that we have had to slowly refactor out of the compiler and like all other software development this won't be instantaneous. We definitely h
50.
by jroesch 11y ago
Unfortunately safety is not the only concern. Idris' tooling is severely limited. There are very few executables written in Idris (and even fewer that aren't bit-rotted), the build tooling and package management are very simple, t
51.
by jroesch 11y ago
Huon is working on SIMD full time at Mozilla this summer as far as I know. We should see more mature support materialize in the next couple of months for sure.
52.
by jroesch 11y ago
The general the coherence rules stop you from defining an implementation that could be possibly defined elsewhere. The important take away implications are: - you can not implement a trait defined in another crate for a type defined in anot
53.
by jroesch 11y ago
I'm the author of the above pull request (as well as other pieces of where clauses), unfortunately there are some internals that need refactoring before we can complete equality constraints, and they weren't the highest priority b
54.
by jroesch 11y ago
I'm pretty sure even when building a JIT Rust would provide advantages. The only unsafe part of JITing is allocating the underlying instruction buffer and marking the memory as executable to the OS. You could still leverage Rust in bui
55.
by jroesch 12y ago
Maybe not well understood by programmers but in the programming language world Go's ideas have been around for over 3 decades.
56.
by jroesch 12y ago
Language choice can be important. If you do the common thing and build a distinct model of your program and prove it correct your guarantees don't hold about the actual implementation. You need a second method to ensure equivalence bet
57.
by jroesch 12y ago
As a current graduate school applicant with a couple of admits to top 10 programs I can confirm this. My GPA looks "low" around a 3.3 cumulative (I have lots of C's in things I deemed unimportant) but I have a relatively high
58.
by jroesch 12y ago
It seems really strange to compare Coq (a functional language for interactive/automatic theorem proving) to plotting tools.
59.
by jroesch 12y ago
The core language is almost completely fixed, and the only real changes will be in unstable areas like associated types. There might be some small API changes but all APIs are marked with stability levels so you should be able to figure out
60.
by jroesch 12y ago
Researchers will often say things like this about techniques they couldn't get working as a way to explain away their failures. Often times some one will come along a couple years later and do exactly what they claimed was impossible

More ›