HackerTrans
TopNewTrendsCommentsPastAskShowJobs

bollu

no profile record

Submissions

Show HN: Formally Verified FPSan

github.com
2 points·by bollu·18 दिन पहले·0 comments

comments

bollu
·3 माह पहले·discuss
Lambda calculus talks about computable functions, where the types of the inputs are typically something discrete, like `Bool` or `Nat`. Here, the domain is the real numbers.
bollu
·6 माह पहले·discuss
please send me an email <[email protected]>. I'm a PhD student at cambridge, and might be able to put you in touch with folks who have positions to hire you as an RA if your research profile fits. even if there isn't an immediate fit, I'm happy to scout around and see if anything pops up. Best, Sid
bollu
·7 माह पहले·discuss
how does one get to conversational level in a week? I would love to know!currently anki-flashcarding my way through italian...
bollu
·7 माह पहले·discuss
Having similar reasoning, I would up writing a tiny-optimizing-compiler tutorial that only explains how to write a middle and back end of a compiler: https://github.com/bollu/tiny-optimising-compiler
bollu
·9 माह पहले·discuss
That's really neat, I hadn't seen the black hole argument before, that's really cute
bollu
·4 वर्ष पहले·discuss
I am very interested to learn about your workflow. What language do you program in? How does acme help programming in this language? Do you have a video or a stream I could watch? I'd love to know!
bollu
·6 वर्ष पहले·discuss
This is very interesting. What other techniques exist, apart from finger-knitting which are unobtrusive and help as an outlet?
bollu
·7 वर्ष पहले·discuss
This only works if your language is strict. With a lazy language like Haskell, you can't statically infer (at least naively with respect to scoping rules) when something lives and dies.

Performing this statically is hard, and GHC tries to do it (Demand analysis).

But without a GC, these sorts of languages would be a no-go, as would logic-based languages like Prolog which need to GC their internal data structures.

While we now have the expertise for eliminating the GC from single threaded strict programs (multi threading in Rust is still quite complex, and you do see Rc<Box<..>> more often than not in these settings, which is essentially refcounting/GC), this _does not scale_ to all models of languages.