pittma

5 ms·

1.
by pittma 1y ago
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!
2.
by pittma 1y ago
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.
3.
by pittma 1y ago
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 its windowing, which includes the formula showing how the w
4.
by pittma 2y ago
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 Sinatra, and then was Jekyll for years. Th
5.
by pittma 6y ago
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 of partiality is okay in Idris, that its typ
6.
by pittma 6y ago
> 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 gets at this to some extent. In rust, partiality causes typ
7.
by pittma 6y ago
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 types is that programs must be /t
8.
by pittma 7y ago
> 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 any such studies? On the contrary! Consider for ins
9.
by pittma 7y ago
It would appear that I accidentally a link or two. https://github.com/auxoncorp/bounded-registers https://github.com/auxoncorp/tnfilt
10.
Using Type-Level Programming in Rust to Make Safer Hardware Abstractions(blog.auxon.io)
8 points by pittma 7y ago|1 comments
11.
by pittma 8y ago
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 adding hardware support in the coming weeks/months.