I think a better summary is that google gave someone the responsibility to ensure AI was developed and used ethically, and didn't give them the power to execute that responsibility. Apparently google did not even give…
What? That post says very clearly at the beginning that hybrids are the preferred approach right now. No one except the NSA actually wants a non-hybrid. Which raises the question what is the NSA up to. Especially since…
California has another distortion. The property value for tax purposes does not change unless you sell. In many other states there is the lesser distortion of property valuearions for tax purposes not being allowed to…
Dijkstra actually had a much more reasonable title on the article. It was the editor of the publication Niklaus Wirth that changed the title to goto considered harmful. Dijkstra was arguing for procedures with a single…
Yeah no. Not really. That is what was tried. The S&P 500 didn't play along. A comparatively small number of index funds & retirement accounts that use them will get caught. The majority won't.
It is worth noting that register coalescing gets a lot of attention in interference graph coloring allocators because they typically have a pre-pass that inserts copies everywhere (because adding copies or spills later…
The big caveat in what I was saying is that it is only the pure graph coloring portion that has an optimal linear time algorithm. Take code in static single assignment form, or another form where it is values that are…
The academic literature on register allocation is scary. First is presented a linear time optimal algorithm for graph coloring then it is claimed better can be done by a O(N^2) algorithm that uses a heuristic. I do…
Not who you asked but I took a quick look. Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime. At the same time their take on loops (you can't write them…
Thank you. That makes things clearer. I especially appreciate the trick of asserting the intermediate truth to help the prover along. As someone who writes software I very much agree that verification of asserts before…
> 36. The use of a program to prove the 4 color theorem will not change mathematics -- it merely demonstrates the theorem, a challenge for a century, is probably not important to mathematicians.
Have you looked at ADA Spark? If you have does it match your intuition of how things should be done? I am slowly working on something where I hope to integrate such a capability for the things that type systems can't…
It is talking about replacing a classic mark/sweep collector for unix domain sockets by something based on Tarjan's Strongly Connected Components.
Weird. The copy I read says they have just deleted that section of their user agreement.
Assuming this is correct that is a very intriguing result. FP64 emulated with FP8 running faster than the native FP64 implementation.
How does it follow that there is no point in trying for formal correctness? In many problems there is an interesting subset that is quickly solvable even when the general case is not. SAT solvers in practice are quick…
Please read the article. The unsolicited security reports are the issue.
Thank you for posting this. I had heard LLMs were finding a lot of bugs very quickly and now I can see what that looks like from a user perspective.
Hooray! A static test fire caught a problem. Crap! There was a serious latent problem for the test fire to find.
Plus pretty blantant plagiarism.
In addition to capabilities, which implemented the principle of least privilege (and keep untrusted code sandboxed by default) there is a need for binary verification. A check that a whatever is downloaded cannot exceed…
My reasing of the study is children with significant gut issues and diagnosed with autism see a significant reduction in symptoms when the gut issues are treated. Which leads me to wonder if for some of these children…
The notification happen when the fix was shipped. That people would prefer to been spoon fed only serious security issues is understandable, but not realistic. A large percentage of kernel fixes have the potential to be…
For everyone getting into the details about how all of this should work please look at RFC7084: Basic Requirements for IPv6 Customer Edge Routers https://www.rfc-editor.org/rfc/rfc7084 It describes in detail what a home…
Language design benefits from parser generators that can point out ambiguities and verify a language is easy to parse.
I think a better summary is that google gave someone the responsibility to ensure AI was developed and used ethically, and didn't give them the power to execute that responsibility. Apparently google did not even give…
What? That post says very clearly at the beginning that hybrids are the preferred approach right now. No one except the NSA actually wants a non-hybrid. Which raises the question what is the NSA up to. Especially since…
California has another distortion. The property value for tax purposes does not change unless you sell. In many other states there is the lesser distortion of property valuearions for tax purposes not being allowed to…
Dijkstra actually had a much more reasonable title on the article. It was the editor of the publication Niklaus Wirth that changed the title to goto considered harmful. Dijkstra was arguing for procedures with a single…
Yeah no. Not really. That is what was tried. The S&P 500 didn't play along. A comparatively small number of index funds & retirement accounts that use them will get caught. The majority won't.
It is worth noting that register coalescing gets a lot of attention in interference graph coloring allocators because they typically have a pre-pass that inserts copies everywhere (because adding copies or spills later…
The big caveat in what I was saying is that it is only the pure graph coloring portion that has an optimal linear time algorithm. Take code in static single assignment form, or another form where it is values that are…
The academic literature on register allocation is scary. First is presented a linear time optimal algorithm for graph coloring then it is claimed better can be done by a O(N^2) algorithm that uses a heuristic. I do…
Not who you asked but I took a quick look. Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime. At the same time their take on loops (you can't write them…
Thank you. That makes things clearer. I especially appreciate the trick of asserting the intermediate truth to help the prover along. As someone who writes software I very much agree that verification of asserts before…
> 36. The use of a program to prove the 4 color theorem will not change mathematics -- it merely demonstrates the theorem, a challenge for a century, is probably not important to mathematicians.
Have you looked at ADA Spark? If you have does it match your intuition of how things should be done? I am slowly working on something where I hope to integrate such a capability for the things that type systems can't…
It is talking about replacing a classic mark/sweep collector for unix domain sockets by something based on Tarjan's Strongly Connected Components.
Weird. The copy I read says they have just deleted that section of their user agreement.
Assuming this is correct that is a very intriguing result. FP64 emulated with FP8 running faster than the native FP64 implementation.
How does it follow that there is no point in trying for formal correctness? In many problems there is an interesting subset that is quickly solvable even when the general case is not. SAT solvers in practice are quick…
Please read the article. The unsolicited security reports are the issue.
Thank you for posting this. I had heard LLMs were finding a lot of bugs very quickly and now I can see what that looks like from a user perspective.
Hooray! A static test fire caught a problem. Crap! There was a serious latent problem for the test fire to find.
Plus pretty blantant plagiarism.
In addition to capabilities, which implemented the principle of least privilege (and keep untrusted code sandboxed by default) there is a need for binary verification. A check that a whatever is downloaded cannot exceed…
My reasing of the study is children with significant gut issues and diagnosed with autism see a significant reduction in symptoms when the gut issues are treated. Which leads me to wonder if for some of these children…
The notification happen when the fix was shipped. That people would prefer to been spoon fed only serious security issues is understandable, but not realistic. A large percentage of kernel fixes have the potential to be…
For everyone getting into the details about how all of this should work please look at RFC7084: Basic Requirements for IPv6 Customer Edge Routers https://www.rfc-editor.org/rfc/rfc7084 It describes in detail what a home…
Language design benefits from parser generators that can point out ambiguities and verify a language is easy to parse.