mietek

18 ms·

181.
by mietek 9y ago
> Machines can’t do cognition Assuming you mean that machines can’t do cognition at present , why do you think we won’t solve this problem in the next 20 years?
182.
by mietek 9y ago
Unfortunately, Adobe bought Macromedia to kill FreeHand, not to continue offering it. http://www.freehandforum.org
183.
by mietek 9y ago
> Apple OS never were much relevant on CAD “Development of ArchiCAD started in 1982 for the original Apple Macintosh.” https://en.wikipedia.org/wiki/ArchiCAD
184.
by mietek 9y ago
The competition has been assimilated. https://en.wikipedia.org/wiki/Altsys https://en.wikipedia.org/wiki/Silicon_Beach_Software https://en.wikipedia.org/wiki/Aldus https:&#x
185.
by mietek 9y ago
> a seminar with a Bond villain Incidentally, the psychologist mentioned in the FB statement appears to have changed his surname to Spectre. https://www.psychol.cam.ac.uk/people/ak823%40cam.ac.uk
186.
by mietek 9y ago
> Zero C is not very special. Zero Kelvin is! I agree that Fredrickson is grasping for relevance. However, 0 °C is special to water-based lifeforms. 0 °C is defined as 273.15 K, or the temperature at which the three phases of water
187.
by mietek 9y ago
> For the language to be useful for proving things, it needs to be strongly normalizing. That means all programs halt—otherwise, you could trivially prove any proposition. Unfortunately that limits its utility as a general purpose progr
188.
by mietek 9y ago
> Show me a web video player that has play and pause buttons that always do what they say when they say it. The only player which ever worked properly — even allowing the user to step through a video frame by frame — was part of Apple’
189.
by mietek 9y ago
This is actually a very good question. The halting problem only applies if you can write a program that loops forever. In other words, the halting problem is only a problem in Turing-complete languages [1], or in languages that admit unco
190.
by mietek 9y ago
Proving theorems in Agda or Idris is like programming in more rigorous variant of Haskell. Proving theorems in Coq is... different.
191.
by mietek 9y ago
> Surveys done shortly after this found that employees who went to the website and discovered they were paid below the median for their peers were much less satisfied on average with their jobs and more likely to express an intent to de
192.
by mietek 9y ago
> Also hunger-gatherers lived right beside the people they knew. They just had to step outside to meet up with friends to socialize. Outside of what, the ministry of hunting and gathering?
193.
by mietek 9y ago
> Programs below this line are considered unfeasible. http://www.inwap.com/pdp10/hbaker/hakmem/proposed.html#item9...
194.
by mietek 9y ago
Dimethyltryptamine video modes?… Sounds about right.
195.
by mietek 9y ago
Why not give Pierce’s “Types and programming languages” a spin?
196.
by mietek 9y ago
This one? https://archive.org/details/byte-magazine-1981-08
197.
by mietek 9y ago
> You'd think that ST itself can be implemented in pure Haskell, maybe with the usual logarithmic slowdown. But unfortunately no one knows how to do it, and there's a strong suspicion that the (pure) type signature of runST ha
198.
by mietek 9y ago
It is great that you are interested in the subject. Please consider joining ##dependent on Freenode IRC.
199.
by mietek 9y ago
Your sketch of a proof does not appear substantially different from the proof given in section 3.1 of the linked paper. Section 3.2 explains that this result does not apply to strongly normalising languages. See also the slides titled “So
200.
by mietek 9y ago
> This can be relatively easily proven to be impossible in any total language. Please provide this proof.
201.
by mietek 10y ago
> The interpretation of Cantor's result will depend upon one's view of mathematics. To constructivists, the argument shows no more than that there is no bijection between the natural numbers and T. https://en.wikip
202.
by mietek 10y ago
As zitterbewegung writes elsewhere in this thread, “there is a Bluetooth radio on the microbit but the runtime was 12k and there wasn't enough space to load micropython and Bluetooth at the same time.”
203.
by mietek 10y ago
Quoting from the fine article, which you clearly have not read: “Finally, the micro:bit’s 16 kB of RAM is quite limiting, at least when using the MicroPython runtime. While writing a moderate-size program I managed to repeatedly exhaust the
204.
by mietek 10y ago
16 KB of memory? The “64” in “Commodore 64”, the name of a computer introduced in 1982, stands for 64 KB of memory. (A 128 KB version followed 3 years later.) It is now 35 years since 1982…
205.
by mietek 10y ago
Good Haskell style already presupposes top-level type annotations.
206.
by mietek 10y ago
Clash. http://www.clash-lang.org
207.
by mietek 10y ago
I agree. One could argue that Agda and Idris are a better interface to the type theory that underlies Coq.
208.
by mietek 10y ago
Could you supply a reference for John Hilliard’s research?
209.
by mietek 10y ago
Is the suspicion that the domes are actually radomes?
210.
by mietek 10y ago
> This is why I think e.g. keyboard instruments should mirror the order of notes between the left and right hand parts. Then you can get away with learning one uniform set of finger motions, instead of two. Funny. I’m currently learn

More ›