Viewing profile — pittma

I am not the original author—this is adapted from an implementation by Shay Gueron, the author of that paper I linked, but I do agree that it's cool!

ymms were used here on purpose! With full-width registers, the IFMA insns have a deleterious effect on frequency, at least in the Icelake timeframe.

Cool stuff! This method is very similar to how AVX-512-optimized RSA implementations work too, as they also have to do Very Large Exponentiations. This paper[1] covers how RSA does…

I have a pretty elaborate Hakyll site with custom routers and all kinds of junk ( https://dpitt.me ), but it's an old site that started as Django, then I built it from scratch with…

Hm, that's not how I'm reading this. An infinite loop is, by definition, partial. What I'm gathering from this is that that stuckness that the typechecker can encounter in the face…

> Totality is orthogonal to dependent types. You can absolutely have non-total programs at the type level: Rust has such programs today in fact! Absolutely, the talk I linked to ge…

You can, in fact, use traits to do type-level programming in Rust[1], but this is type-level programming; it isn't /dependent/ types. The biggest "blocker" for using dependent type…

> Are you saying there have been studies that show Haskell's type system has not been correlated to higher correctness than say Java or Python, or are you saying you are unaware of…

It would appear that I accidentally a link or two. https://github.com/auxoncorp/bounded-registers https://github.com/auxoncorp/tnfilt

feL4 developer here. Happy to field questions, and to note that we'll keep introducing and extending the ergonomics for building complex applications, configuring platforms, and ad…