| --- Log opened Wed Apr 08 00:00:04 2020 |
| 00:00 | | Emmy [Emmy@Nightstar-9p7hb1.direct-adsl.nl] has quit [Ping timeout: 121 seconds] |
| 00:16 | <&jeroud> | TheWatcher: Use gnolam's open communications standard.~ |
| 00:22 | | abudhabi_ [abudhabi@Nightstar-7nkq9k.de] has quit [Operation timed out] |
| 00:55 | | macdjord|slep is now known as macdjord |
| 01:30 | | catalyst [catalyst@Nightstar-v6lb30.cable.virginm.net] has joined #code |
| 01:40 | | Degi [Degi@Nightstar-cputkc.dyn.telefonica.de] has quit [Operation timed out] |
| 01:42 | | Degi [Degi@Nightstar-0ft46n.dyn.telefonica.de] has joined #code |
| 01:53 | | Pinkhair [user1@Nightstar-g7hdo5.dyn.optonline.net] has joined #code |
| 01:55 | | Pink [user1@Nightstar-g7hdo5.dyn.optonline.net] has quit [Ping timeout: 121 seconds] |
| 02:03 | | Vornicus [Vorn@ServerAdministrator.Nightstar.Net] has quit [Connection closed] |
| 04:07 | | celticminstrel [celticminst@Nightstar-80avij.dsl.bell.ca] has quit [[NS] Quit: And lo! The computer falls into a deep sleep, to awake again some other day!] |
| 07:05 | | ToxicFrog [ToxicFrog@ServerAdministrator.Nightstar.Net] has quit [Ping timeout: 121 seconds] |
| 07:16 | | ToxicFrog [ToxicFrog@ServerAdministrator.Nightstar.Net] has joined #code |
| 07:16 | | mode/#code [+ao ToxicFrog ToxicFrog] by ChanServ |
| 08:38 | | Vornicus [Vorn@ServerAdministrator.Nightstar.Net] has joined #code |
| 08:39 | | mode/#code [+qo Vornicus Vornicus] by ChanServ |
| 08:56 | | catalyst [catalyst@Nightstar-v6lb30.cable.virginm.net] has quit [[NS] Quit: -a- IRC for Android 2.1.55] |
| 13:41 | | celticminstrel [celticminst@Nightstar-80avij.dsl.bell.ca] has joined #code |
| 13:41 | | mode/#code [+o celticminstrel] by ChanServ |
| 13:44 | < NSGuest33425> | McMartin (or anyone else): I have a project at work where one possible angle is formally verified code generation. (The compiler is written in Haskell.) do you know of a good place to start investigating how to go about this? I only took an intro course to type theory and formal semantics, but I'm eager to learn. |
| 13:45 | | NSGuest33425 is now known as sshine |
| 13:45 | | mode/#code [+o sshine] by ChanServ |
| 14:04 | | Kindamoody is now known as Kindamoody|out |
| 15:30 | <&McMartin> | I am vaguely aware that some projects of this nature have been attempted, but what knowledge I have of it is a decade out of date |
| 15:31 | <&McMartin> | Program analysis research in my salad days of 200X was mostly about cheating the halting problem and I had little contact with formal methods |
| 17:04 | | VirusJTG [VirusJTG@Nightstar-42s.jso.104.208.IP] has quit [Connection closed] |
| 17:04 | | VirusJTG [VirusJTG@Nightstar-42s.jso.104.208.IP] has joined #code |
| 17:04 | | mode/#code [+ao VirusJTG VirusJTG] by ChanServ |
| 17:26 | | Emmy [Emmy@Nightstar-9p7hb1.direct-adsl.nl] has joined #code |
| 18:01 | | Kindamoody|out is now known as Kindamoody |
| 18:26 | | Pinkhair [user1@Nightstar-g7hdo5.dyn.optonline.net] has quit [Ping timeout: 121 seconds] |
| 18:40 | | Pink [user1@Nightstar-g7hdo5.dyn.optonline.net] has joined #code |
| 19:36 | <@sshine> | McMartin, oh, shoot. I recall you did stuff with Java, and I thought it might have been formal methods. |
| 19:37 | <@sshine> | McMartin, I talked with the postdoc on our team and he suggested I use Liquid Haskell to prove some weaker things first. which suits me fine, because my current goal then consists of things I already know but haven't done. unlike stuff I don't know and haven't done. |
| 19:39 | <@sshine> | also, it seems that to get anywhere, I'll need to create a call-graph generator and an Ethereum VM interpreter, which are... totally nice pet projects. |
| 19:40 | <@sshine> | I am so happy about my new job. I work from home, so it doesn't feel like work. I write open source Haskell, so it doesn't feel like work. and when I'm not doing that, I sit and chat with people about potential projects, which feels more like coffee-break chat and doesn't feel like work. |
| 20:42 | | * Alek wonders if there's still time to apply for Code In Place, and if it's worthwhile. |
| 21:11 | <@sshine> | what's that? |
| 21:12 | <@sshine> | ah, google told me. |
| 21:12 | <@sshine> | https://compedu.stanford.edu/codeinplace/announcement/ -- signing up works. |
| 21:13 | <@sshine> | also, computer scientists who let you pick "non-binary" for any category is progressive! |
| 21:21 | | VirusJTG_ [VirusJTG@Nightstar-42s.jso.104.208.IP] has joined #code |
| 21:22 | | VirusJTG [VirusJTG@Nightstar-42s.jso.104.208.IP] has quit [Ping timeout: 121 seconds] |
| 21:51 | <&jeroud> | Even "internal representation of data"?~ |
| 21:54 | <&ToxicFrog> | typedef enum { YES, NO, MAYBE } Gender; |
| 21:55 | <@Tamber> | YES, NO, MAYBE, I_DONT_KNOW, CAN_YOU_REPEAT_THE_QUESTION, YOURE_NOT_THE_BOSS_OF_ME |
| 21:57 | <~Vornicus> | life is unfair / so I just stare / at the stain in the wall where / the tv'd been / but ever since / we've moved in it's been empty |
| 21:57 | <@Tamber> | :D |
| 22:00 | <~Vornicus> | (I only got to "where" from memory, sadly) |
| 22:14 | <@ErikMesoy> | Obligatory tri-state boolean: https://docs.microsoft.com/en-us/dotnet/api/microsoft.office.core.msotristate |
| 22:16 | <~Vornicus> | https://thedailywtf.com/articles/What_Is_Truth_0x3f_ |
| 22:18 | <@Tamber> | And the lonely voice of youth cries, "What is truth?"~ |
| 22:48 | | Emmy [Emmy@Nightstar-9p7hb1.direct-adsl.nl] has quit [Ping timeout: 121 seconds] |
| 23:34 | <&[R]> | http://thedailywtf.com/articles/Circling-the-Solution <-- I found something I was looking for, for a while |
| --- Log closed Thu Apr 09 00:00:05 2020 |