Less ambitious in one sense, since it allows you to use the full power of higher order separation logic (which no one is trying to claim is a usable general purpose programming language) in proving the unsafe specs. But it also means a more complicated semantic typing model.
Yeah, maybe it more has to do with having a champion in the field. Substructural type systems didn’t seem to have many champions in academia when Rust came on the scene.
-
-
which means you faced this uphill battle, which sucks. but once this energy barrier is overcome, subsequent papers have a much easier time.
-
Which ironically was easier to do outside academia—building industry adoption basically forced academics to take it seriously. BTW I’m aiming to do the same with Pathfinder—the graphics community has a bias against 2D and incorrectly considers it a solved problem. Same dynamic.
- 3 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.