akiarie

9 ms·

61.
Show HN: Xr0 – Vanilla C Made Safe with Annotations(xr0.dev)
17 points by akiarie 3y ago|13 comments
62.
Ask HN: What buggy software is relied upon by the most people?
6 points by akiarie 3y ago|6 comments
63.
What I Learned Implementing Lex(0.rwstream.com)
3 points by akiarie 3y ago|2 comments
64.
Dijkstra: Two Views of Programming (EWD540)(raboof.github.io)
1 points by akiarie 3y ago|0 comments
65.
GPT-4 Khan Academy in Depth Demo(youtube.com)
1 points by akiarie 4y ago|0 comments
66.
by akiarie 4y ago
We're looking at this. Some very fascinating stuff. Somewhere at the beginning of "The Calculi of Lambda Conversion" Church talks about the fact that quantification can be reduced to lambdas. I have not read to the end of the
67.
by akiarie 4y ago
> How does i2 compare with other languages used in verification? I have to plead a measure of ignorance here as the context for my response, though we are working to understand the existing languages. Perhaps what distinguishes i2 from t
68.
by akiarie 4y ago
I think the challenge is it isn't completely obvious to me that starting with 0 is pedagogically correct, though it is so logically. `y >= x + y` is different from `y != x + y`; the former says that addition (of natural numbers) is
69.
by akiarie 4y ago
You raise two fine points. > Natural numbers should start with 0 [0]. I agree 100% with Dijkstra about where the numbers should begin. In fact, here's an early draft in which we were using 0 instead of 1: [0]. The reason we ended up
70.
Show HN: i2forge – A Platform for Verified Reasoning(i2forge.com)
35 points by akiarie 4y ago|13 comments
71.
by akiarie 4y ago
Ken Thompson's famous paper on implementing regular expressions is surprisingly simple and yet extremely sophisticated at the same time. The "heart" of the method he proposed was the use of a stack in order to compile the exp
72.
Show HN: A Regex-to-Golang compiler based on Thompson's algorithm(github.com)
1 points by akiarie 4y ago|1 comments